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

[bugfix] level 0 conflict in mcsat weren't detected

Browse source
This commit is contained in:
Guillaume Bury 2015-02-09 17:10:45 +01:00
parent 5f155f6bde
commit 9c8e970b8d
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
solver/mcsolver.ml
View file

@ -327,7 +327,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
let backtrack_lvl is_uip = function let backtrack_lvl is_uip = function
| [] -> 0 | [] -> 0
| a :: r when not is_uip -> a.var.level - 1 | a :: r when not is_uip -> max (a.var.level - 1) 0
| a :: [] -> 0 | a :: [] -> 0
| a :: b :: r -> assert(a.var.level <> b.var.level); b.var.level | a :: b :: r -> assert(a.var.level <> b.var.level); b.var.level
@ -342,9 +342,10 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
| _ -> false | _ -> false
in in
try while true do try while true do
let _, atoms = max_lvl_atoms !c in let lvl, atoms = max_lvl_atoms !c in
L.debug 15 "Current conflict clause :"; L.debug 15 "Current conflict clause :";
List.iter (fun a -> L.debug 15 " |- %a" St.pp_atom a) !c; List.iter (fun a -> L.debug 15 " |- %a" St.pp_atom a) !c;
if lvl = 0 then raise Exit;
match atoms with match atoms with
| [] | _ :: [] -> | [] | _ :: [] ->
L.debug 15 "Found UIP clause"; L.debug 15 "Found UIP clause";