From 4127db2153bdb8f686fffcd2c775ba8718f8fca6 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 11 Feb 2019 08:44:15 -0600 Subject: [PATCH] Revert "fix: catch `E_unsat` in assume, if one adds an empty clause" This reverts commit 5d7e34584bdbfd8326fbbf7f3314d93ac79597ce. --- src/core/Internal.ml | 20 +++++++------------- 1 file changed, 7 insertions(+), 13 deletions(-) diff --git a/src/core/Internal.ml b/src/core/Internal.ml index ca61e3f9..16bf0300 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -1988,19 +1988,13 @@ module Make(Plugin : PLUGIN) with E_sat -> () let assume st cnf lemma = - 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] *) + 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 (* Check satisfiability *) let check_clause c =