From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 14 Apr 2010 01:43:48 +0000 (+0000)
Subject: Bugfix. r284 or earlier removed checking of counter-examples. i.e. -d did nothing.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=014055f856afb5480e26b885a12cd1f87f64e838;p=francis%2Fstp.git

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 4241a42..0511378 100644
--- 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());