3 files changed, 13 insertions, 14 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index f12aec08..5b22b782 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1413,7 +1413,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       // Somewhat gross to create these all the time, but fine till we
       // switch to an internal rep.
       ConstantInt *ci = ConstantInt::get(si->getCondition()->getType(),
-                                         CE->getConstantValue());
+                                         CE->getZExtValue());
       unsigned index = si->findCaseValue(ci);
       transferToBasicBlock(si->getSuccessor(index), si->getParent(), state);
     } else {
@@ -2688,11 +2688,10 @@ void Executor::executeAlloc(ExecutionState &state,
     assert(success && "FIXME: Unhandled solver failure");
     (void) success;
     
-    // Try and start with a small example
-    while (example->getConstantValue() > 128) {
-      ref<ConstantExpr> tmp = 
-        ConstantExpr::alloc(example->getConstantValue() >> 1, 
-                            example->getWidth());
+    // Try and start with a small example.
+    Expr::Width W = example->getWidth();
+    while (example->Ugt(ConstantExpr::alloc(128, W))->isTrue()) {
+      ref<ConstantExpr> tmp = example->LShr(ConstantExpr::alloc(1, W));
       bool res;
       bool success = solver->mayBeTrue(state, EqExpr::create(tmp, size), res);
       assert(success && "FIXME: Unhandled solver failure");      
@@ -3225,7 +3224,7 @@ void Executor::doImpliedValueConcretization(ExecutionState &state,
         assert(!os->readOnly && 
                "not possible? read only object with static read?");
         ObjectState *wos = state.addressSpace.getWriteable(mo, os);
-        wos->write(CE->getConstantValue(), it->second);
+        wos->write(CE, it->second);
       }
     }
   }
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index d8cf0bdb..49198df8 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -187,7 +187,7 @@ const UpdateList &ObjectState::getUpdates() const {
       if (!Value)
         break;
 
-      Contents[Index->getConstantValue()] = Value;
+      Contents[Index->getZExtValue()] = Value;
     }
 
     // FIXME: We should unique these, there is no good reason to create multiple
@@ -400,7 +400,7 @@ void ObjectState::write8(unsigned offset, uint8_t value) {
 void ObjectState::write8(unsigned offset, ref<Expr> value) {
   // can happen when ExtractExpr special cases
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
-    write8(offset, (uint8_t) CE->getConstantValue());
+    write8(offset, (uint8_t) CE->getZExtValue(8));
   } else {
     setKnownSymbolic(offset, value.get());
       
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 2ee73457..d2c68b77 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -198,7 +198,7 @@ SpecialFunctionHandler::readStringAtAddress(ExecutionState &state,
     cur = executor.toUnique(state, cur);
     assert(isa<ConstantExpr>(cur) && 
            "hit symbolic char while reading concrete string");
-    buf[i] = cast<ConstantExpr>(cur)->getConstantValue();
+    buf[i] = cast<ConstantExpr>(cur)->getZExtValue(8);
   }
   buf[i] = 0;
   
@@ -441,7 +441,7 @@ void SpecialFunctionHandler::handleSetForking(ExecutionState &state,
   ref<Expr> value = executor.toUnique(state, arguments[0]);
   
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
-    state.forkDisabled = !CE->getConstantValue();
+    state.forkDisabled = CE->isZero();
   } else {
     executor.terminateStateOnError(state, 
                                    "klee_set_forking requires a constant arg",
@@ -607,7 +607,7 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state,
     } else {
       ref<Expr> chk = op.first->getBoundsCheckPointer(address, 
                                                       cast<ConstantExpr>(size)->getConstantValue());
-      if (!cast<ConstantExpr>(chk)->getConstantValue()) {
+      if (!chk->isTrue()) {
         executor.terminateStateOnError(state,
                                        "check_memory_access: memory error",
                                        "ptr.err",
@@ -636,8 +636,8 @@ void SpecialFunctionHandler::handleDefineFixedObject(ExecutionState &state,
   assert(isa<ConstantExpr>(arguments[1]) &&
          "expect constant size argument to klee_define_fixed_object");
   
-  uint64_t address = cast<ConstantExpr>(arguments[0])->getConstantValue();
-  uint64_t size = cast<ConstantExpr>(arguments[1])->getConstantValue();
+  uint64_t address = cast<ConstantExpr>(arguments[0])->getZExtValue();
+  uint64_t size = cast<ConstantExpr>(arguments[1])->getZExtValue();
   MemoryObject *mo = executor.memory->allocateFixed(address, size, state.prevPC->inst);
   executor.bindObjectInState(state, mo, false);
   mo->isUserSpecified = true; // XXX hack;