diff options
| -rw-r--r-- | include/klee/ArrayExprOptimizer.h | 3 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 8 |
2 files changed, 5 insertions, 6 deletions
diff --git a/include/klee/ArrayExprOptimizer.h b/include/klee/ArrayExprOptimizer.h index 2d8a9014..36c26484 100644 --- a/include/klee/ArrayExprOptimizer.h +++ b/include/klee/ArrayExprOptimizer.h @@ -72,8 +72,7 @@ private: unordered_map<unsigned, ref<Expr>> cacheReadExprOptimized; public: - void optimizeExpr(const ref<Expr> &e, ref<Expr> &result, - bool valueOnly = false); + void optimizeExpr(const ref<Expr> &e, ref<Expr> &result, bool valueOnly); private: bool diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 506fa12f..f0335812 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1100,7 +1100,7 @@ ref<Expr> Executor::toUnique(const ExecutionState &state, OptimizeArray == INDEX) && !isa<ConstantExpr>(cond)) { ref<Expr> res; - optimizer.optimizeExpr(cond, res); + optimizer.optimizeExpr(cond, res, false); if (res.get()) { cond = res; } @@ -1612,7 +1612,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { OptimizeArray == INDEX) && !isa<ConstantExpr>(cond)) { ref<Expr> result; - optimizer.optimizeExpr(cond, result); + optimizer.optimizeExpr(cond, result, false); if (result.get()) { cond = result; } @@ -1765,7 +1765,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { OptimizeArray == INDEX) && !isa<ConstantExpr>(match)) { ref<Expr> result; - optimizer.optimizeExpr(match, result); + optimizer.optimizeExpr(match, result, false); if (result.get()) { match = result; } @@ -1800,7 +1800,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { OptimizeArray == INDEX) && !isa<ConstantExpr>(defaultValue)) { ref<Expr> result; - optimizer.optimizeExpr(defaultValue, result); + optimizer.optimizeExpr(defaultValue, result, false); if (result.get()) { defaultValue = result; } |