fix bugs

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

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

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

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

test/c/malloc_aligned.t

@@ -1,2 +1,2 @@
-  $ owi c ./malloc_aligned.c
+  $ owi c ./malloc_aligned.c -w1
   All OK