From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 2 May 2011 14:14:58 +0000 (+0000)
Subject: Bugfix. Rarely we get the wrong answer; I got two broken instances in 140 days of... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=9ffa221d9d6928d4c05669b2d8df531125ed517d;p=francis%2Fstp.git

Bugfix. Rarely we get the wrong answer; I got two broken instances in 140 days of fuzzing. This fixes those two instances, but, almost any change to STP fixes it, i.e. causes the problem to go away.

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 726977b..661e4be 100644
--- 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);