2 files changed, 15 insertions, 16 deletions
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index 08a9ef7c..6e52dc32 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -363,12 +363,12 @@ protected:
     // value cannot be part of the assignment.
     if (index >= array.size)
       return ReadExpr::create(UpdateList(&array, 0), 
-                              ConstantExpr::alloc(index, Expr::Int32));
+                              ConstantExpr::alloc(index, array.getDomain()));
       
     std::map<const Array*, CexObjectData*>::iterator it = objects.find(&array);
     return ConstantExpr::alloc((it == objects.end() ? 127 : 
                                 it->second->getPossibleValue(index)),
-                               Expr::Int8);
+                               array.getRange());
   }
 
 public:
@@ -384,19 +384,19 @@ protected:
     // value cannot be part of the assignment.
     if (index >= array.size)
       return ReadExpr::create(UpdateList(&array, 0), 
-                              ConstantExpr::alloc(index, Expr::Int32));
+                              ConstantExpr::alloc(index, array.getDomain()));
       
     std::map<const Array*, CexObjectData*>::iterator it = objects.find(&array);
     if (it == objects.end())
       return ReadExpr::create(UpdateList(&array, 0), 
-                              ConstantExpr::alloc(index, Expr::Int32));
+                              ConstantExpr::alloc(index, array.getDomain()));
 
     CexValueData cvd = it->second->getExactValues(index);
     if (!cvd.isFixed())
       return ReadExpr::create(UpdateList(&array, 0), 
-                              ConstantExpr::alloc(index, Expr::Int32));
+                              ConstantExpr::alloc(index, array.getDomain()));
 
-    return ConstantExpr::alloc(cvd.min(), Expr::Int8);
+    return ConstantExpr::alloc(cvd.min(), array.getRange());
   }
 
 public:
@@ -1109,13 +1109,14 @@ FastCexSolver::computeInitialValues(const Query& query,
   // Propogation found a satisfying assignment, compute the initial values.
   for (unsigned i = 0; i != objects.size(); ++i) {
     const Array *array = objects[i];
+    assert(array);
     std::vector<unsigned char> data;
     data.reserve(array->size);
 
     for (unsigned i=0; i < array->size; i++) {
       ref<Expr> read = 
         ReadExpr::create(UpdateList(array, 0),
-                         ConstantExpr::create(i, Expr::Int32));
+                         ConstantExpr::create(i, array->getDomain()));
       ref<Expr> value = cd.evaluatePossible(read);
       
       if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 22b1545f..025c70f2 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);
@@ -493,8 +494,6 @@ Solver *klee::createDummySolver() {
 
 class STPSolverImpl : public SolverImpl {
 private:
-  /// The solver we are part of, for access to public information.
-  STPSolver *solver;
   VC vc;
   STPBuilder *builder;
   double timeout;
@@ -502,7 +501,7 @@ private:
   SolverRunStatus runStatusCode;
 
 public:
-  STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides = true);
+  STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides = true);
   ~STPSolverImpl();
   
   char *getConstraintLog(const Query&);
@@ -526,9 +525,8 @@ static void stp_error_handler(const char* err_msg) {
   abort();
 }
 
-STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides)
-  : solver(_solver),
-    vc(vc_createValidityChecker()),
+STPSolverImpl::STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides)
+  : vc(vc_createValidityChecker()),
     builder(new STPBuilder(vc, _optimizeDivides)),
     timeout(0.0),
     useForkedSTP(_useForkedSTP),
@@ -565,7 +563,7 @@ STPSolverImpl::~STPSolverImpl() {
 /***/
 
 STPSolver::STPSolver(bool useForkedSTP, bool optimizeDivides)
-  : Solver(new STPSolverImpl(this, useForkedSTP, optimizeDivides))
+  : Solver(new STPSolverImpl(useForkedSTP, optimizeDivides))
 {
 }