diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2015-09-18 14:53:16 +0200 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2015-09-18 14:53:16 +0200 |
commit | 090cd7310cf8257081c87a64985d588bd749566b (patch) | |
tree | 9f0e2f1c837733bb0e4875eb635f4f814571bb4f /lib | |
parent | 89d023e59cf61c17744ec8dca3451f25eeba58b0 (diff) | |
parent | 4ddf8d3ccc054cd1be6bae25844373ed2488360a (diff) | |
download | klee-090cd7310cf8257081c87a64985d588bd749566b.tar.gz |
Merge pull request #275 from MartinNowack/fix_empty_constraints_indep_solver
Allow to generate initial values for queries with empty constraint set.
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Solver/IndependentSolver.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index cfe1bb16..a7685e46 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -454,6 +454,12 @@ bool IndependentSolver::computeInitialValues(const Query& query, std::vector< std::vector<unsigned char> > &values, bool &hasSolution){ std::list<IndependentElementSet> * factors = new std::list<IndependentElementSet>; + + // We assume the query has a solution except proven differently + // This is important in case we don't have any constraints but + // we need initial values for requested array objects. + hasSolution = true; + getAllIndependentConstraintsSets(query, factors); //Used to rearrange all of the answers into the correct order std::map<const Array*, std::vector<unsigned char> > retMap; |