From c68f034ead5eeb191810b1327702d76a20b41a37 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 19 Mar 2024 14:10:33 +0100 Subject: [PATCH] Add a link to issue 1063 --- src/lib/reasoners/sat_solver_util.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/lib/reasoners/sat_solver_util.ml b/src/lib/reasoners/sat_solver_util.ml index 1011abd64c..7fe8eaca31 100644 --- a/src/lib/reasoners/sat_solver_util.ml +++ b/src/lib/reasoners/sat_solver_util.ml @@ -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;