Make get_value sound by not returning a formula is false when it is a…

…bsent from the environment (#942)

src/lib/reasoners/fun_sat.ml

@@ -1852,7 +1852,12 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     | Ty.Tbool ->
       begin
         match ME.find_opt t env.gamma with
-        | None -> Some E.faux
+        | None ->
+          begin
+            match ME.find_opt (E.neg t) env.gamma with
+            | None -> None
+            | Some _ -> Some E.faux
+          end
         | Some _ -> Some E.vrai
       end
     | _ -> None

src/lib/reasoners/satml_frontend.ml

@@ -1389,7 +1389,12 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     | Ty.Tbool ->
       begin
         match ME.find_opt t env.gamma with
-        | None -> Some E.faux
+        | None ->
+          begin
+            match ME.find_opt (E.neg t) env.gamma with
+            | None -> None
+            | Some _ -> Some E.faux
+          end
         | Some _ -> Some E.vrai
       end
     | _ -> None

tests/models/bool/bool1.models.expected

@@ -3,7 +3,7 @@ unknown
 (
   (define-fun q () Bool false)
 )
-((notp false)
+((notp unknown)
  (notnq true))
 
 

tests/models/bool/bool2.models.expected

@@ -2,5 +2,5 @@
 unknown
 (
 )
-((notx false))
+((notx unknown))
 

tests/models/bool/bool3.models.expected

@@ -5,5 +5,5 @@ unknown
   (define-fun y () Bool true)
 )
 ((foo true)
- (bar false))
+ (bar unknown))