[Bool] fix:special case for cl=true and cl=false work (bad or pattern ...)

Makefile

 
 
 PACKAGES=oUnit zarith ocamlgraph str #-package lablgtk2
-OPTIONS=-tag annot -no-sanitize -tag debug -use-ocamlfind -cflags -w,+a-4-9 -cflags -warn-error,+5+10+8 -cflag -bin-annot -j 8
+OPTIONS=-tag annot -no-sanitize -tag debug -use-ocamlfind -cflags -w,+a-4-9 -cflags -warn-error,+5+10+8+12 -cflag -bin-annot -j 8
 #OPTIONS += -cflags -warn-error,+a
 DIRECTORIES=src src/util src/inputlang/altergo src/inputlang/dimacs_cnf src/inputlang/smtlib2 tests src/cmd fuzz
 OCAMLBUILD=ocamlbuild \

src/bool.ml

@@ -183,7 +183,7 @@ module Th = struct
       | None -> raise (Found (cl,b))
     ) l
 
-  let bcp d l absorbent =
+  let _bcp d l absorbent =
     try
       let res = IArray.fold (fun acc cl ->
         let cl = Delayed.find d cl in
@@ -750,20 +750,26 @@ module ConClause = struct
     let s = get_con s t c2 in
     GRequested s
 
-  let propacl t age cl rcl =
-    match cl, rcl with
-    | _true, cl | cl, _true when Cl.equal _true cl_true ->
+  let propacl t _age clo rcl =
+    match clo, rcl with
+    | (_true, cl) when Cl.equal _true cl_true ->
       ComputeConflict.set_dec_cho t dom cl chobool cl;
       GRequested (Cl.M.singleton cl true)
-    | _false, cl | cl, _false when Cl.equal _false cl_false ->
+    | (cl, _true) when Cl.equal _true cl_true ->
+      ComputeConflict.set_dec_cho t dom cl chobool cl;
+      GRequested (Cl.M.singleton cl true)
+    | (_false, cl) when Cl.equal _false cl_false ->
+      ComputeConflict.set_dec_cho t dom cl chobool cl;
+      GRequested (Cl.M.singleton cl false)
+    | (cl, _false) when Cl.equal _false cl_false ->
       ComputeConflict.set_dec_cho t dom cl chobool cl;
       GRequested (Cl.M.singleton cl false)
     | _ ->
-      let eq = !mk_permanent_equality (cl,rcl) in
+      let eq = !mk_permanent_equality (clo,rcl) in
       ComputeConflict.set_dec_cho t dom eq chobool eq;
       GRequested (Cl.M.singleton eq true)
 
-  let propasem t age sem v cl =
+  let propasem t _age sem v cl =
     (** TODO ty bool if sem is bool? *)
     let eq = !mk_permanent_equality (cl,new_permanent sem v (Cl.ty cl)) in
     ComputeConflict.set_dec_cho t dom eq chobool eq;

src/uninterp.ml

@@ -301,8 +301,12 @@ module ExpSubst = struct
         let fty = Cl.ty f in
         let gty = Cl.ty g in
         let deps = Deps.empty in
+        let rl = get_sem t sem v in
+        let ty = match rl with CRepr -> assert false (* get_sem *)
+                             | CMerge (rcl,_,_,_) -> Cl.ty rcl in
         let deps =
-          Equality.GenEquality.sem_def t deps age (get_sem t sem v) in
+          (** TODO separate the first Merge(UF) from the others(GenEquality)? *)
+          Equality.GenEquality.sem t deps age sem v rl ty in
         let deps =
           Equality.GenEquality.repr t deps age f (get_cl_repr t f) fty in
         let deps =