about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
authorMartin Nowack <martin.nowack@gmail.com>2015-08-30 02:11:45 +0200
committerMartin Nowack <martin@se.inf.tu-dresden.de>2015-09-05 02:08:36 +0200
commit4ddf8d3ccc054cd1be6bae25844373ed2488360a (patch)
tree9f0e2f1c837733bb0e4875eb635f4f814571bb4f /lib/Solver
parent89d023e59cf61c17744ec8dca3451f25eeba58b0 (diff)
downloadklee-4ddf8d3ccc054cd1be6bae25844373ed2488360a.tar.gz
Allow to generate initial values with empty constraint set
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/IndependentSolver.cpp6
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;