From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 11 Sep 2009 20:50:30 +0000 (+0000)
Subject: minor edits
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=63ac0641ed01d2c274a07d938a43c1371d75d24d;p=francis%2Fstp.git

minor edits

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

diff --git a/src/abstraction-refinement/AbstractionRefinement.cpp b/src/abstraction-refinement/AbstractionRefinement.cpp
index d441d43..58a3973 100644
--- a/src/abstraction-refinement/AbstractionRefinement.cpp
+++ b/src/abstraction-refinement/AbstractionRefinement.cpp
@@ -257,31 +257,36 @@ namespace BEEV
     SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED;
     for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(),
 	  iend=GlobalList_Of_FiniteLoops.end(); i!=iend; i++)
-    {
-      //cout << "The number of abs-refinement limit is " << num_absrefine << endl;
-      for(int absrefine_count=0;absrefine_count < num_absrefine; absrefine_count++) 
-	{
-	  ASTNodeMap ParamToCurrentValMap;
-	  retvec =  SATBased_FiniteLoop_Refinement(SatSolver,
-						   original_input,
-						   *i,
-						   &ParamToCurrentValMap,
-						   true); //absrefine flag
-	  ASTNode retformula = 
-	    (retvec.size() == 1) ?
-	    retvec[0] : CreateNode(AND,retvec);
-	  //SimplifyFormula(CreateNode(AND,Allretvec),false,NULL);
-	  retformula = TransformFormula_TopLevel(retformula);
-
-	  //Add the return value of all loops to the SAT Solver
-	  res = 
-	    CallSAT_ResultCheck(SatSolver, retformula, original_input);
-	  if(SOLVER_UNDECIDED != res) 
-	    {
+      {
+	//cout << "The number of abs-refinement limit is " << num_absrefine << endl;
+	for(int absrefine_count=0;absrefine_count < num_absrefine; absrefine_count++) 
+	  {
+	    ASTNodeMap ParamToCurrentValMap;
+	    retvec =  SATBased_FiniteLoop_Refinement(SatSolver,
+						     original_input,
+						     *i,
+						     &ParamToCurrentValMap,
+						     true); //absrefine flag
+	    ASTNode retformula = 
+	      (retvec.size() == 1) ?
+	      retvec[0] : CreateNode(AND,retvec);
+	    //SimplifyFormula(CreateNode(AND,Allretvec),false,NULL);
+	    retformula = TransformFormula_TopLevel(retformula);
+	    
+	    //Add the return value of all loops to the SAT Solver
+	    res = 
+	      CallSAT_ResultCheck(SatSolver, retformula, original_input);
+	    if(SOLVER_UNDECIDED != res) 
+	      {
 	      return res;
-	    }	  
-	} //end of absrefine count
+	      }
+	  } //end of absrefine count
+    } //End of For
 
+    for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(),
+	  iend=GlobalList_Of_FiniteLoops.end(); i!=iend; i++)
+    {
+      //The abs-refine didn't finish the job. Add the remaining axioms
       ASTNodeMap ParamToCurrentValMap;
       retvec =  SATBased_FiniteLoop_Refinement(SatSolver,
 					       original_input,
@@ -300,7 +305,7 @@ namespace BEEV
 	{
 	  return res;
 	}	  	
-      } //End of For()
+    } //End of For()
 
     return res;
   } //end of SATBased_AllFiniteLoops_Refinement()