small checks

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);

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)