diff options
author | Dan Liew <delcypher@gmail.com> | 2014-04-24 12:12:22 +0100 |
---|---|---|
committer | Dan Liew <delcypher@gmail.com> | 2014-04-24 12:12:22 +0100 |
commit | 292e8cc794f01df94ca02279f5833d7a460a62f9 (patch) | |
tree | 80400e7fa9b69edd1ecdb3600ca88244f533c389 /lib/Solver/Solver.cpp | |
parent | 7f44b9346356c91f633c6de6939c33a45756ae7e (diff) | |
parent | 2795655e567c3cdbfe3d4815edd83b4f4cdbb542 (diff) | |
download | klee-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.cpp | 5 |
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); |