From 479f4c1b79d5562739c98da51b18fff2534c09bc Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 15 Apr 2016 11:54:00 +0200 Subject: [PATCH] small checks --- solver/internal.ml | 1 + solver/res.ml | 3 ++- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/solver/internal.ml b/solver/internal.ml index 4b1d7082..84b34c81 100644 --- a/solver/internal.ml +++ b/solver/internal.ml @@ -290,6 +290,7 @@ module Make match a.var.reason with | Bcp (Some cl) -> atoms, cl :: history, max lvl cl.c_level | Semantic 0 -> atoms, history, lvl + | Bcp None -> assert false | _ -> Log.debugf 0 "Unexpected semantic propagation at level 0: %a" (fun k->k St.pp_atom a); diff --git a/solver/res.ml b/solver/res.ml index 03192e21..25d0da33 100644 --- a/solver/res.ml +++ b/solver/res.ml @@ -91,7 +91,8 @@ module Make(St : Solver_types.S) = struct let l = List.map (fun a -> match St.(a.var.reason) with | St.Bcp Some d -> d - | _ -> assert false) l + | St.Bcp None -> assert false + | St.Semantic _ -> assert false) l in St.make_clause (fresh_pcl_name ()) [] 0 true (St.History (c :: l)) (List.fold_left (fun i c -> max i c.St.c_level) 0 l)