From c2299e09d851d4c6144fc7b39e6c0ddeb30c71b1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Fri, 11 Oct 2024 15:31:45 +0200 Subject: [PATCH] rm th_entailed in new_vars --- src/lib/reasoners/satml.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index cd061c17c..fa6394aa5 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -2087,6 +2087,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct Vec.push env.vars v; assert (not (is_semantic v.pa)); insert_var_order env v; + accu (* match th_entailed tenv0 v.pa with | None -> accu | Some (c, sz) -> @@ -2095,7 +2096,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct else unit_cnf, c :: nunit_cnf [@ocaml.ppwarning "Issue: BAD decision_level, in particular, \ - if minimal-bj is ON"] + if minimal-bj is ON"] *) ) (unit_cnf, nunit_cnf) new_v in (* This assert is no longer true because some of the vars in the