fixed some bugs in the user-guided refinement implementation

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 0fadf1b37edb962101ed967f3115ff13c0943a49..09cb5198100466ba5bab15a7ead02ad085814dc5 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -214,10 +214,17 @@ namespace BEEV {
         return res;
       }
 
-    FatalError("TopLevelSTPAux: reached the end without proper conclusion:"
-               "either a divide by zero in the input or a bug in STP");
-    //bogus return to make the compiler shut up
-    return SOLVER_ERROR;
+    if(!bm->UserFlags.num_absrefine_flag)
+      {
+       FatalError("TopLevelSTPAux: reached the end without proper conclusion:"
+                  "either a divide by zero in the input or a bug in STP");
+       //bogus return to make the compiler shut up
+       return SOLVER_ERROR;
+      }
+    else
+      {
+       return res;
+      }
   } //End of TopLevelSTPAux
 
   //UserGuided abstraction refinement
@@ -286,6 +293,14 @@ namespace BEEV {
       (RemainingFormulasVec.size() == 1) ?
       RemainingFormulasVec[0] : bm->CreateNode(AND, RemainingFormulasVec);
     res = TopLevelSTPAux(NewSolver, RemainingFormulas, original_input);
-    return res;
+    
+    if(SOLVER_UNDECIDED != res)
+      {
+       return res;
+      }
+    
+    FatalError("TopLevelSTPAux: reached the end without proper conclusion:"
+              "either a divide by zero in the input or a bug in STP");    
+    return SOLVER_ERROR;
   } //End of UserGuided_AbsRefine()
 }; //end of namespace

diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp
index f922a9bcbd34b4883d4eb6dcd97927c9d501d6d6..c05172267951a5d265f63c6cc15cf33e77723ce9 100644 (file)
--- a/src/absrefine_counterexample/AbstractionRefinement.cpp
+++ b/src/absrefine_counterexample/AbstractionRefinement.cpp
@@ -44,11 +44,11 @@ namespace BEEV
                                const ASTNode& inputAlreadyInSAT, 
                                const ASTNode& original_input) {
     //printf("doing array read refinement\n");
-    if (!bm->UserFlags.arrayread_refinement_flag)
-      {
-        FatalError("SATBased_ArrayReadRefinement: "\
-                   "Control should not reach here");
-      }
+    // if (!bm->UserFlags.arrayread_refinement_flag)
+    //       {
+    //         FatalError("SATBased_ArrayReadRefinement: "     \
+    //                    "Control should not reach here");
+    //       }
     ASTVec FalseAxiomsVec, RemainingAxiomsVec;
     RemainingAxiomsVec.push_back(ASTTrue);
     FalseAxiomsVec.push_back(ASTTrue);