about summary refs log tree commit diff homepage
path: root/lib/Solver/Solver.cpp
diff options
context:
space:
mode:
authorDan Liew <delcypher@gmail.com>2014-04-24 12:12:22 +0100
committerDan Liew <delcypher@gmail.com>2014-04-24 12:12:22 +0100
commit292e8cc794f01df94ca02279f5833d7a460a62f9 (patch)
tree80400e7fa9b69edd1ecdb3600ca88244f533c389 /lib/Solver/Solver.cpp
parent7f44b9346356c91f633c6de6939c33a45756ae7e (diff)
parent2795655e567c3cdbfe3d4815edd83b4f4cdbb542 (diff)
downloadklee-292e8cc794f01df94ca02279f5833d7a460a62f9.tar.gz
Merge pull request #112 from hpalikareva/domain-range-extra
Removing a few more hard-coded values for domains and ranges of Array ob...
Diffstat (limited to 'lib/Solver/Solver.cpp')
-rw-r--r--lib/Solver/Solver.cpp5
1 files changed, 3 insertions, 2 deletions
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 22b1545f..c61b6b1c 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -407,11 +407,12 @@ ValidatingSolver::computeInitialValues(const Query& query,
     std::vector< ref<Expr> > bindings;
     for (unsigned i = 0; i != values.size(); ++i) {
       const Array *array = objects[i];
+      assert(array);
       for (unsigned j=0; j<array->size; j++) {
         unsigned char value = values[i][j];
         bindings.push_back(EqExpr::create(ReadExpr::create(UpdateList(array, 0),
-                                                           ConstantExpr::alloc(j, Expr::Int32)),
-                                          ConstantExpr::alloc(value, Expr::Int8)));
+                                                           ConstantExpr::alloc(j, array->getDomain())),
+                                          ConstantExpr::alloc(value, array->getRange())));
       }
     }
     ConstraintManager tmp(bindings);