From 7673bddf8222877f002f280d9bdb97121e192057 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 10 Feb 2019 18:03:11 -0600 Subject: [PATCH] fix: catch `E_unsat` in assume, if one adds an empty clause --- src/core/Internal.ml | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/src/core/Internal.ml b/src/core/Internal.ml index 16bf0300..ca61e3f9 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -1988,13 +1988,19 @@ module Make(Plugin : PLUGIN) with E_sat -> () let assume st cnf lemma = - List.iter - (fun l -> - let atoms = List.rev_map (mk_atom st) l in - let c = Clause.make_permanent atoms (Hyp lemma) in - Log.debugf debug (fun k -> k "(@[sat.assume-clause@ @[%a@]@])" Clause.debug c); - Vec.push st.clauses_to_add c) - cnf + try + List.iter + (fun l -> + let atoms = List.rev_map (mk_atom st) l in + let c = Clause.make_permanent atoms (Hyp lemma) in + Log.debugf debug (fun k -> k "(@[sat.assume-clause@ @[%a@]@])" Clause.debug c); + Vec.push st.clauses_to_add c) + cnf + with + | E_unsat (US_false c) -> + st.unsat_at_0 <- Some c + | E_unsat (US_local _) -> + assert false (* assumptions should only be present in [solve] *) (* Check satisfiability *) let check_clause c =