From 59c4db1464d1e563213fc72e513d90d3feba7014 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 6 Jan 2011 00:11:41 +0000 Subject: [PATCH] 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 --- .../AbstractionRefinement.cpp | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp index ce6823e..a5ffcd3 100644 --- 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 -- 2.47.3