Skip to content

Commit

Permalink
SMT: Restart solver if --record_hints changes
Browse files Browse the repository at this point in the history
Since we now decide whether or not to pass set `produce-unsat-cores`
according to it, which is a flag persistent across an invocation, we
must restart the solver if it changes.
  • Loading branch information
mtzguido committed Feb 4, 2025
1 parent 3ce8045 commit 44bfb5c
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions src/smtencoding/FStarC.SMTEncoding.Solver.fst
Original file line number Diff line number Diff line change
Expand Up @@ -1269,6 +1269,7 @@ type solver_cfg = {
valid_elim : bool;
z3version : string;
context_pruning : bool;
record_hints : bool;
}
let _last_cfg : ref (option solver_cfg) = BU.mk_ref None
Expand All @@ -1282,6 +1283,7 @@ let get_cfg env : solver_cfg =
; valid_elim = Options.smtencoding_valid_elim ()
; z3version = Options.z3_version ()
; context_pruning = Options.Ext.enabled "context_pruning"
; record_hints = Options.record_hints ()
}
let save_cfg env =
Expand Down

0 comments on commit 44bfb5c

Please sign in to comment.