Skip to content

Commit

Permalink
revert: use separate context for tmp solver for query generation
Browse files Browse the repository at this point in the history
  • Loading branch information
daejunpark committed Oct 10, 2024
1 parent 6f6b12a commit bd2287a
Showing 1 changed file with 2 additions and 5 deletions.
7 changes: 2 additions & 5 deletions src/halmos/sevm.py
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,6 @@
BoolVal,
CheckSatResult,
Concat,
Context,
Extract,
Function,
If,
Expand Down Expand Up @@ -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:
Expand Down

0 comments on commit bd2287a

Please sign in to comment.