From 0bdb296e78436da37f36655f19ae06c6e033ec2d Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Thu, 19 Nov 2009 20:54:25 +0000 Subject: [PATCH] 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 --- src/STPManager/STP.cpp | 25 +++++++++++++++---- .../AbstractionRefinement.cpp | 10 ++++---- 2 files changed, 25 insertions(+), 10 deletions(-) diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 0fadf1b..09cb519 100644 --- 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 f922a9b..c051722 100644 --- 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); -- 2.47.3