diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index f62053a5..68f3ed9d 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -26,7 +26,6 @@ BoolVal, CheckSatResult, Concat, - Context, Extract, Function, If, @@ -736,11 +735,9 @@ def to_smt2(self, args) -> SMTQuery: if args.cache_solver: # TODO: investigate whether a separate context is necessary here - tmp_solver = create_solver(ctx=Context()) + tmp_solver = create_solver() for cond in self.conditions: - tmp_solver.assert_and_track( - cond.translate(tmp_solver.ctx), str(cond.get_id()) - ) + tmp_solver.assert_and_track(cond, str(cond.get_id())) query = tmp_solver.to_smt2() tmp_solver.reset() else: