Skip to content

Commit

Permalink
Add a link to issue 1063
Browse files Browse the repository at this point in the history
  • Loading branch information
Halbaroth committed Mar 19, 2024
1 parent 5e73f14 commit c68f034
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion src/lib/reasoners/sat_solver_util.ml
Original file line number Diff line number Diff line change
Expand Up @@ -149,7 +149,9 @@ let get_value (type a) (module SAT : S with type t = a) env l =
necessary [0] and the SMT statement `get-value` can be called only in
SAT mode, so we have to reset all the decisions of the solver here.
Before resetting the decisions, we save the boolean model for sake
of optimization. *)
of optimization.
See issue: https://github.com/OCamlPro/alt-ergo/issues/1063 *)
let bmdl = SAT.get_boolean_model env in
SAT.reset_decisions env;
assert_model (module SAT) env mdl;
Expand Down

0 comments on commit c68f034

Please sign in to comment.