Bugfix. Would segfault if a vector was empty.

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

diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp
index ce6823e29ea7f51e1a25fba57aaf64b8fe7ae1f9..a5ffcd3dbad62a2025deb475c2365a8c7b7174f5 100644 (file)
--- a/src/absrefine_counterexample/AbstractionRefinement.cpp
+++ b/src/absrefine_counterexample/AbstractionRefinement.cpp
@@ -136,14 +136,16 @@ namespace BEEV
                                }
           }
       }
-    ASTNode RemainingAxioms = 
-      (RemainingAxiomsVec.size() > 1) ? 
-      bm->CreateNode(AND, RemainingAxiomsVec) : RemainingAxiomsVec[0];
-    bm->ASTNodeStats("adding remaining readaxioms to SAT: ", RemainingAxioms);
-    return CallSAT_ResultCheck(SatSolver, 
-                               RemainingAxioms, 
-                               original_input,
-                               tosat);
+    if (RemainingAxiomsVec.size() > 0)
+    {
+               ASTNode RemainingAxioms =
+                               (RemainingAxiomsVec.size() > 1) ? bm->CreateNode(AND,
+                                               RemainingAxiomsVec) : RemainingAxiomsVec[0];
+               bm->ASTNodeStats("adding remaining readaxioms to SAT: ",
+                               RemainingAxioms);
+               return CallSAT_ResultCheck(SatSolver, RemainingAxioms, original_input,
+                               tosat);
+       }
   } //end of SATBased_ArrayReadRefinement