Proof-checking code; fixups of segfaults and missing functionality in proof generation; fix bug 285.

* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line

1 files changed, 5 insertions, 2 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index d1baaa2e9..bf66629dd 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -108,6 +108,10 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       ! opts[options::threadArgv].empty() ) {
     throw OptionException("Thread options cannot be used with sequential CVC4.  Please build and use the portfolio binary `pcvc4'.");
   }
+# else
+  if( opts[options::checkProofs] ) {
+    throw OptionException("Cannot run portfolio in check-proofs mode.");
+  }
 # endif
 
   progName = opts[options::binary_name].c_str();
@@ -201,8 +205,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
              << "Notice: ...the experimental --incremental-parallel option.\n";
     exprMgr = new ExprManager(opts);
     pExecutor = new CommandExecutor(*exprMgr, opts);
-  }
-  else {
+  } else {
     exprMgr = new ExprManager(threadOpts[0]);
     pExecutor = new CommandExecutorPortfolio(*exprMgr, opts, threadOpts);
   }