Bugfix. Rarely we get the wrong answer; I got two broken instances in 140 days of...

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

diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index 726977ba0a50065b3c55dffc977345f74ff41f11..661e4be2b00bdfc8483708cc709fd9ada424efed 100644 (file)
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -872,6 +872,7 @@ namespace BEEV
       {
         bm->GetRunTimes()->start(RunTimes::CounterExampleGeneration);
         CounterExampleMap.clear();
+        ComputeFormulaMap.clear();
 
         ToSAT::ASTNodeToSATVar satVarToSymbol =
             tosat->SATVar_to_SymbolIndexMap();
@@ -882,7 +883,6 @@ namespace BEEV
             PrintSATModel(SatSolver, m);
           }
         //check if the counterexample is good or not
-        ComputeFormulaMap.clear();
         if (bm->counterexample_checking_during_refinement)
           bm->bvdiv_exception_occured = false;
         ASTNode orig_result = ComputeFormulaUsingModel(original_input);