From 2fc41c8c1bcf5721d5305d43eb02994305f78203 Mon Sep 17 00:00:00 2001
From: zapashcanon <leo@ndrs.fr>
Date: Mon, 10 Feb 2025 17:44:41 +0100
Subject: [PATCH] fix bugs

---
 src/cmd/cmd_conc.ml                     |  2 +-
 src/concolic/concolic_choice.ml         |  4 +---
 src/symbolic/symbolic_choice.ml         |  3 ++-
 src/symbolic/symbolic_path_condition.ml | 16 ++++++++++------
 test/c/malloc_aligned.t                 |  2 +-
 5 files changed, 15 insertions(+), 12 deletions(-)

diff --git a/src/cmd/cmd_conc.ml b/src/cmd/cmd_conc.ml
index 35fca2a8d..0ed538aa4 100644
--- a/src/cmd/cmd_conc.ml
+++ b/src/cmd/cmd_conc.ml
@@ -339,7 +339,7 @@ let find_node_to_run tree =
   loop tree []
 
 let pc_model solver pc =
-  let pc = Concolic_choice.pc_to_exprs pc |> Symbolic_path_condition.to_set in
+  let pc = Concolic_choice.pc_to_exprs pc in
   match Solver.check solver pc with
   | `Unsat | `Unknown -> None
   | `Sat ->
diff --git a/src/concolic/concolic_choice.ml b/src/concolic/concolic_choice.ml
index 723ce34df..e72b3ef9e 100644
--- a/src/concolic/concolic_choice.ml
+++ b/src/concolic/concolic_choice.ml
@@ -43,9 +43,7 @@ let pc_elt_to_expr = function
   | Assume c -> Some c
   | Assert _ -> None
 
-let pc_to_exprs pc =
-  List.filter_map pc_elt_to_expr pc
-  |> List.fold_left Symbolic_path_condition.add Symbolic_path_condition.empty
+let pc_to_exprs pc = List.filter_map pc_elt_to_expr pc |> Smtml.Expr.Set.of_list
 
 type shared_thread_info =
   { memories : Symbolic_memory.collection
diff --git a/src/symbolic/symbolic_choice.ml b/src/symbolic/symbolic_choice.ml
index e7b538396..58fadb6b9 100644
--- a/src/symbolic/symbolic_choice.ml
+++ b/src/symbolic/symbolic_choice.ml
@@ -399,7 +399,8 @@ module Make (Thread : Thread_intf.S) = struct
         true
       in
       let false_branch =
-        let* () = add_pc (Symbolic_value.Bool.not v) in
+        let v = Symbolic_value.Bool.not v in
+        let* () = add_pc v in
         let* () = add_breadcrumb 0l in
         let+ () = check_reachability v in
         false
diff --git a/src/symbolic/symbolic_path_condition.ml b/src/symbolic/symbolic_path_condition.ml
index fc27f6853..51a74d84c 100644
--- a/src/symbolic/symbolic_path_condition.ml
+++ b/src/symbolic/symbolic_path_condition.ml
@@ -24,15 +24,19 @@ let add (pc : t) (c : Symbolic_value.vbool) : t =
   let c = Smtml.Expr.Set.singleton c in
   union_on_all_syms c pc symbols
 
+(* Turns all constraints into a set *)
+let to_set pc =
+  Union_find.merge_all_values ~empty:Smtml.Expr.Set.empty
+    ~merge:Smtml.Expr.Set.union pc
+
 (* Return the set of constraints from [pc] that are relevant for [c]. *)
 let slice (pc : t) (c : Symbolic_value.vbool) : Smtml.Expr.Set.t =
   match Smtml.Expr.get_symbols [ c ] with
-  | [] -> (* TODO: not sure what to do here *) Smtml.Expr.Set.empty
+  | [] -> Smtml.Expr.Set.add c (to_set pc)
   | sym0 :: _tl -> (
+    (* we need only the first symbol as all the other one should have been merged with it *)
     match Union_find.find_opt sym0 pc with
-    | None -> Smtml.Expr.Set.empty
+    | None ->
+      (* if there is a symbol, it should have been added to the union-find structure before *)
+      assert false
     | Some s -> s )
-
-let to_set pc =
-  Union_find.merge_all_values ~empty:Smtml.Expr.Set.empty
-    ~merge:Smtml.Expr.Set.union pc
diff --git a/test/c/malloc_aligned.t b/test/c/malloc_aligned.t
index 4ae05c6d3..b3d3b3a3c 100644
--- a/test/c/malloc_aligned.t
+++ b/test/c/malloc_aligned.t
@@ -1,2 +1,2 @@
-  $ owi c ./malloc_aligned.c
+  $ owi c ./malloc_aligned.c -w1
   All OK