about summary refs log tree commit diff homepage
path: root/lib/Solver/Solver.cpp
diff options
context:
space:
mode:
authorHristina Palikareva <h.palikareva@imperial.ac.uk>2014-04-16 17:56:13 +0100
committerHristina Palikareva <h.palikareva@imperial.ac.uk>2014-04-16 18:11:55 +0100
commitaa8cc67c0d8c16388ebe670757327a81f774d0ee (patch)
tree1ee1a08cff55c96cbc169a88a9516c0b933295ad /lib/Solver/Solver.cpp
parent7f44b9346356c91f633c6de6939c33a45756ae7e (diff)
downloadklee-aa8cc67c0d8c16388ebe670757327a81f774d0ee.tar.gz
Removing a few more hard-coded values for domains and ranges of Array objects
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);