src/HOL/SMT/lib/scripts/cert_smt.pl

worker_next: treat wait for work_available as Sleeping, not Waiting;
max_threads: simple adaptive scheme between m and 2 * m;

#
# 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"; }