Only create counter example in terms of original formula if needed.

include/stp/STPManager/UserDefinedFlags.h

@@ -73,10 +73,12 @@ struct UserDefinedFlags // not copyable
 
   // construct the counterexample in terms of original variable based
   // on the counterexample returned by SAT solver
-  bool construct_counterexample_flag;
   bool print_counterexample_flag;
   bool print_binary_flag;
 
+  //This is derived from other settings.
+  bool construct_counterexample_flag;
+
   // if this option is true then print the way dawson wants using a
   // different printer. do not use this printer.
   bool print_arrayval_declaredorder_flag;
@@ -214,11 +216,12 @@ struct UserDefinedFlags // not copyable
     // arraywrite_refinement_flag = true;
 
     // check the counterexample against the original input to STP
-    check_counterexample_flag = true;
+    check_counterexample_flag = false;
 
     // construct the counterexample in terms of original variable based
     // on the counterexample returned by SAT solver
-    construct_counterexample_flag = true;
+    construct_counterexample_flag = false;
+
     print_counterexample_flag = false;
     print_binary_flag = false;
 
@@ -259,6 +262,7 @@ struct UserDefinedFlags // not copyable
 
     tseitin_are_decision_variables_flag = true;
 
+
     // If cryptominisat is installed, use it as default, otherwise minisat.
 #ifdef USE_CRYPTOMINISAT
     solver_to_use = CRYPTOMINISAT5_SOLVER;

lib/AbsRefineCounterExample/CounterExample.cpp

@@ -1046,11 +1046,13 @@ AbsRefine_CounterExample::CallSAT_ResultCheck(
 
   if (!sat)
   {
-    // PrintOutput(true);
     return SOLVER_VALID;
   }
   else if (SatSolver.okay())
   {
+    if (!bm->UserFlags.construct_counterexample_flag)
+      return SOLVER_INVALID;
+
     bm->GetRunTimes()->start(RunTimes::CounterExampleGeneration);
     CounterExampleMap.clear();
     ComputeFormulaMap.clear();
@@ -1067,7 +1069,6 @@ AbsRefine_CounterExample::CallSAT_ResultCheck(
     if (!(ASTTrue == orig_result || ASTFalse == orig_result))
       FatalError("TopLevelSat: Original input must compute to "
                  "true or false against model");
-
     bm->GetRunTimes()->stop(RunTimes::CounterExampleGeneration);
 
     // if the counterexample is indeed a good one, then return

lib/STPManager/STP.cpp

@@ -310,6 +310,15 @@ STP::TopLevelSTPAux(SATSolver& NewSolver, const ASTNode& original_input)
     assert(!arrayops);
   }
 
+  if (bm->UserFlags.check_counterexample_flag || bm->UserFlags.print_counterexample_flag || (arrayops && !removed))
+    bm->UserFlags.construct_counterexample_flag = true;
+  else
+    bm->UserFlags.construct_counterexample_flag = false;
+
+  #ifndef NDEBUG
+      bm->UserFlags.construct_counterexample_flag = true;
+  #endif
+
   // Run size reducing just once.
   inputToSat = sizeReducing(inputToSat, bvSolver.get(), pe.get());
   unsigned initial_difficulty_score = difficulty.score(inputToSat,bm);