From 7f05da56cc702bcaf31fb9828c0fbfd3e90883e5 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 11 Feb 2019 08:50:12 -0600 Subject: [PATCH] fix: cache E_unsat in direct `add_clause` functions --- src/core/Internal.ml | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/src/core/Internal.ml b/src/core/Internal.ml index 16bf0300..a13f210f 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -2087,13 +2087,21 @@ module Make(Plugin : PLUGIN) in { Solver_intf.unsat_conflict; get_proof; unsat_assumptions; } - let[@inline] add_clause_a st c lemma : unit = - let c = Clause.make_a ~flags:0 c (Hyp lemma) in - add_clause_ st c + let add_clause_a st c lemma : unit = + try + let c = Clause.make_a ~flags:0 c (Hyp lemma) in + add_clause_ st c + with + | E_unsat (US_false c) -> + st.unsat_at_0 <- Some c - let[@inline] add_clause st c lemma : unit = - let c = Clause.make_permanent c (Hyp lemma) in - add_clause_ st c + let add_clause st c lemma : unit = + try + let c = Clause.make_permanent c (Hyp lemma) in + add_clause_ st c + with + | E_unsat (US_false c) -> + st.unsat_at_0 <- Some c let solve ?(assumptions=[]) (st:t) : res = cancel_until st 0;