simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-10 05:03:59 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Better error message

Browse source
This commit is contained in:
Guillaume Bury 2015-01-29 15:44:54 +01:00
parent 803b61c7dc
commit 436dc49111
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
solver/mcsolver.ml
View file

@ -370,7 +370,10 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
var_bump_activity a.var;
history := d :: !history;
c := res
| _ -> assert false
| _ ->
L.debug 0 "Found %d resolution lits" (List.length tmp);
List.iter (fun c -> L.debug 0 " |- %a" St.pp_atom c) tmp;
assert false
end
| Bcp None -> L.debug 15 "Decision : %a" St.pp_atom a
| Semantic _ -> L.debug 15 "Semantic propagation : %a" St.pp_atom a)