simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 12:24:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Revert "fix: catch E_unsat in assume, if one adds an empty clause"

Browse source 
This reverts commit 5d7e34584bdbfd8326fbbf7f3314d93ac79597ce.
This commit is contained in:
Simon Cruanes 2019-02-11 08:44:15 -06:00 • committed by Guillaume Bury
parent 7673bddf82
commit 4127db2153
1 changed files with 7 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/core/Internal.ml
View file

@ -1988,19 +1988,13 @@ module Make(Plugin : PLUGIN)
with E_sat -> () with E_sat -> ()
let assume st cnf lemma = let assume st cnf lemma =
try List.iter
List.iter (fun l ->
(fun l -> let atoms = List.rev_map (mk_atom st) l in
let atoms = List.rev_map (mk_atom st) l in let c = Clause.make_permanent atoms (Hyp lemma) in
let c = Clause.make_permanent atoms (Hyp lemma) in Log.debugf debug (fun k -> k "(@[sat.assume-clause@ @[<hov 2>%a@]@])" Clause.debug c);
Log.debugf debug (fun k -> k "(@[sat.assume-clause@ @[<hov 2>%a@]@])" Clause.debug c); Vec.push st.clauses_to_add c)
Vec.push st.clauses_to_add c) cnf
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 *) (* Check satisfiability *)
let check_clause c = let check_clause c =