fix regression tests, support fallback mode for proofs

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index b9e951f7b1dc16f1d3061ed839713270aa8fd391..7bc711910a7a12b116c9849a7845e40e40fab106 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -139,10 +139,6 @@ 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();
@@ -242,16 +238,32 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   pExecutor = new CommandExecutor(*exprMgr, opts);
 # else
   vector<Options> threadOpts = parseThreadSpecificOptions(opts);
+  bool useParallelExecutor = true;
+  // incremental?
   if(opts.wasSetByUser(options::incrementalSolving) &&
      opts[options::incrementalSolving] &&
      !opts[options::incrementalParallel]) {
     Notice() << "Notice: In --incremental mode, using the sequential solver unless forced by...\n"
              << "Notice: ...the experimental --incremental-parallel option.\n";
-    exprMgr = new ExprManager(opts);
-    pExecutor = new CommandExecutor(*exprMgr, opts);
-  } else {
+    useParallelExecutor = false;
+  }
+  // proofs?
+  if(opts[options::checkProofs]) {
+    if(opts[options::fallbackSequential]) {
+      Warning() << "Warning: Falling back to sequential mode, as cannot run portfolio in check-proofs mode.\n";
+      useParallelExecutor = false;
+    }
+    else {
+      throw OptionException("Cannot run portfolio in check-proofs mode.");
+    }
+  }
+  // pick appropriate one
+  if(useParallelExecutor) {
     exprMgr = new ExprManager(threadOpts[0]);
     pExecutor = new CommandExecutorPortfolio(*exprMgr, opts, threadOpts);
+  } else {
+    exprMgr = new ExprManager(opts);
+    pExecutor = new CommandExecutor(*exprMgr, opts);
   }
 # endif
 

diff --git a/test/regress/run_regression b/test/regress/run_regression
index b6fb735fe5885b48f39296a52773c2006900eb58..9204fe33c5048d8a036d8f376709e10dd56da910 100755 (executable)
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -239,6 +239,7 @@ if [ "$proof" = yes ]; then
        ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--incremental' &>/dev/null &&
        ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--unconstrained-simp' &>/dev/null &&
        ! expr " $CVC4_REGRESSION_ARGS $command_line" : '.* -[a-zA-Z]*i' &>/dev/null &&
+       ! expr "$BINARY" : '.*pcvc4' &>/dev/null &&
        ! expr "$benchmark" : '.*\.sy$' &>/dev/null; then
       # later on, we'll run another test with --check-proofs on
       check_proofs=true
@@ -248,6 +249,7 @@ if [ "$proof" = yes ]; then
        ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--incremental' &>/dev/null &&
        ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--unconstrained-simp' &>/dev/null &&
        ! expr " $CVC4_REGRESSION_ARGS $command_line" : '.* -[a-zA-Z]*i' &>/dev/null &&
+       ! expr "$BINARY" : '.*pcvc4' &>/dev/null &&
        ! expr "$benchmark" : '.*\.sy$' &>/dev/null; then
       # later on, we'll run another test with --check-unsat-cores on
       check_unsat_cores=true