Bugfix. r284 or earlier removed checking of counter-examples. i.e. -d did nothing.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@671 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index 4241a424c2d0b61ac76b64cc8d868248489eb291..0511378821c3063cc33727c3d1de386082d6beae 100644 (file)
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -657,16 +657,6 @@ namespace BEEV
 
   void AbsRefine_CounterExample::CheckCounterExample(bool t)
   {
-    // FIXME: Code is more useful if enable flags are check OUTSIDE
-    // the method.  If I want to check a counterexample somewhere, I
-    // don't want to have to set the flag in order to make it actualy
-    // happen!
-    printf("checking counterexample\n");
-    if (!bm->UserFlags.check_counterexample_flag)
-      {
-        return;
-      }
-
     //input is valid, no counterexample to check
     if (bm->ValidFlag)
       return;
@@ -676,6 +666,10 @@ namespace BEEV
       FatalError("CheckCounterExample: "\
                  "No CounterExample to check", ASTUndefined);
     const ASTVec c = bm->GetAsserts();
+
+    if (bm->UserFlags.stats_flag)
+       printf("checking counterexample\n");
+
     for (ASTVec::const_iterator
            it = c.begin(), itend = c.end(); it != itend; it++)
       if (ASTFalse == ComputeFormulaUsingModel(*it))
@@ -979,7 +973,8 @@ namespace BEEV
         // invalid
         if (ASTTrue == orig_result)
           {
-            //CheckCounterExample(SatSolver.okay());
+            if (bm->UserFlags.check_counterexample_flag)
+                               CheckCounterExample(SatSolver.okay());
             //PrintOutput(false);
             PrintCounterExample(SatSolver.okay());
             PrintCounterExample_InOrder(SatSolver.okay());