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

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

Browse source
This commit is contained in:
Simon Cruanes 2019-02-10 18:03:11 -06:00 • committed by Guillaume Bury
parent ea98f6f027
commit 7673bddf82
1 changed files with 13 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/core/Internal.ml
View file

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