Skip to content

Commit e7c5faa

Browse files
committed
graph-refine: fix order of evaluation for saving SMT proof check
1 parent 6720935 commit e7c5faa

File tree

1 file changed

+5
-4
lines changed

1 file changed

+5
-4
lines changed

rep_graph.py

+5-4
Original file line numberDiff line numberDiff line change
@@ -1124,12 +1124,13 @@ def test_hyp_imps (self, imps):
11241124
for (hyps, hyp) in imps]))
11251125

11261126
if save_smt_proof_checks[0]:
1127+
save_imps = [
1128+
{ 'meta': None, 'term': smt_expr(hyp_, {}, self.solv) }
1129+
for (_, hyp_) in interp_imps
1130+
]
11271131
obj = {
1132+
'imps': save_imps,
11281133
'setup': [ msg for (msg, _) in self.solv.replayable ],
1129-
'imps': [
1130-
{ 'meta': None, 'term': smt_expr(hyp_, {}, self.solv) }
1131-
for (_, hyp_) in interp_imps
1132-
],
11331134
}
11341135
save = save_smt_proof_checks[0]
11351136
save (self.p, obj)

0 commit comments

Comments
 (0)