fail on unsimplified expressions

Author: redianthus

src/symbolic/symbolic_path_condition.ml

@@ -16,16 +16,14 @@ let empty : t =
 
 (* TODO: should we make some normalization here? *)
 (* TODO: it would be better to split the conjunctions in many sub-conditions *)
-let add ({ uf; set } as old : t) (c : Symbolic_value.bool) : t =
+let add ({ uf; set } : t) (c : Symbolic_value.bool) : t =
   match Smtml.Expr.get_symbols [ c ] with
   | [] ->
-    (* TODO: It means Smt.ml did not properly simplified a expression... *)
-    (* assert false *)
-    (* For now, we use this, it should be removed and assert false should be used instead later *)
-    Logs.debug (fun m ->
+    (* It means Smt.ml did not properly simplified a expression! *)
+    Logs.err (fun m ->
       m "an expression was not simplified by smtml: %a" Symbolic_value.pp_int32
         c );
-    old
+    assert false
   | hd :: tl ->
     let set = Smtml.Expr.Set.add c set in
     (* We add the first symbol to the UF *)
@@ -46,16 +44,14 @@ let add ({ uf; set } as old : t) (c : Symbolic_value.bool) : t =
 let to_set { uf = _; set } = set
 
 (* Return the set of constraints from [pc] that are relevant for [c]. *)
-let slice ({ uf; set } : t) (c : Symbolic_value.bool) : Smtml.Expr.Set.t =
+let slice ({ uf; set = _ } : t) (c : Symbolic_value.bool) : Smtml.Expr.Set.t =
   match Smtml.Expr.get_symbols [ c ] with
   | [] ->
-    (* TODO: It means Smt.ml did not properly simplified a expression... *)
-    (* assert false *)
-    (* For now, we use this, it should be removed and assert false should be used instead later *)
-    Logs.debug (fun m ->
+    (* It means Smt.ml did not properly simplified a expression... *)
+    Logs.err (fun m ->
       m "an expression was not simplified by smtml: %a" Symbolic_value.pp_int32
         c );
-    Smtml.Expr.Set.add c set
+    assert false
   | sym0 :: _tl -> (
     (* we need only the first symbol as all the others should have been merged with it *)
     match Union_find.find_opt sym0 uf with