added proof reconstructon for Z3,
added certificates for simpler re-checking of proofs (no need to invoke external solvers),
added examples and certificates for all examples,
removed Unsynchronized.ref (in smt_normalize.ML)
#
# 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"; }