--- a/src/HOL/SMT/lib/scripts/cert_smt.pl Tue Feb 02 11:38:38 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-#
-# Author: Sascha Boehme, TU Muenchen
-#
-# Fake SMT solver: check that input matches previously computed input and
-# and return previously computed output.
-#
-
-use strict;
-use File::Compare;
-
-
-# arguments
-
-my $cert_path = $ARGV[0];
-my $new_problem = $ARGV[1];
-
-
-# check content of new problem file against old problem file
-
-my $old_problem = $cert_path;
-my $old_proof = $cert_path . ".proof";
-
-if (-e $old_problem and compare($old_problem, $new_problem) == 0) {
- if (-e $old_proof) {
- open FILE, "<$old_proof";
- foreach (<FILE>) {
- print $_;
- }
- close FILE;
- }
- else { print "ERROR: unable to open proof file\n"; }
-}
-else { print "ERROR: bad problem\n"; }