add a shortcut to avoid checking the false branch on an assume

Author: redianthus

src/symbolic/symbolic_choice.ml

@@ -430,7 +430,8 @@ module Make (Thread : Thread_intf.S) = struct
     | `Unknown -> assert false
 
   let select_inner ~explore_first ?(with_breadcrumbs = true)
-    (cond : Symbolic_value.bool) ~prio_true ~prio_false =
+    ~check_only_true_branch (cond : Symbolic_value.bool) ~prio_true ~prio_false
+      =
     let v = Smtml.Expr.simplify cond in
     match Smtml.Expr.view v with
     | Val True -> return true
@@ -465,15 +466,21 @@ module Make (Thread : Thread_intf.S) = struct
       in
 
       let true_branch = branch v true prio_true in
-      let false_branch = branch (Symbolic_value.Bool.not v) false prio_false in
-      let* thread in
-      Thread.incr_path_count thread;
-      if explore_first then choose true_branch false_branch
-      else choose false_branch true_branch
+
+      if check_only_true_branch then true_branch
+      else
+        let false_branch =
+          branch (Symbolic_value.Bool.not v) false prio_false
+        in
+        let* thread in
+        Thread.incr_path_count thread;
+        if explore_first then choose true_branch false_branch
+        else choose false_branch true_branch
   [@@inline]
 
   let select (cond : Symbolic_value.bool) ~prio_true ~prio_false =
     select_inner cond ~explore_first:true ~prio_true ~prio_false
+      ~check_only_true_branch:false
   [@@inline]
 
   let summary_symbol (e : Smtml.Expr.t) =
@@ -537,6 +544,7 @@ module Make (Thread : Thread_intf.S) = struct
     let* assertion_true =
       select_inner c ~with_breadcrumbs:false ~explore_first:false
         ~prio_true:Prio.Default ~prio_false:Prio.Default
+        ~check_only_true_branch:false
     in
     if assertion_true then return ()
     else
@@ -551,10 +559,9 @@ module Make (Thread : Thread_intf.S) = struct
 
   let assume c =
     let* assertion_true =
-      select_inner c ~with_breadcrumbs:false
-        ~explore_first:false
-          (* TODO: make the prio false very low, we are not interested in such branches *)
+      select_inner c ~with_breadcrumbs:false ~explore_first:true
         ~prio_true:Prio.Default ~prio_false:Prio.Default
+        ~check_only_true_branch:true
     in
     if assertion_true then return () else stop
 end

test/replay/assert_false.t

@@ -1,8 +1,8 @@
   $ owi sym assert_false.wat -w1
   owi: [ERROR] Assert failure: (i32.lt_u symbol_1 symbol_0)
   model {
-    symbol symbol_0 i32 1107329090
-    symbol symbol_1 i32 -1040154559
+    symbol symbol_0 i32 134252706
+    symbol symbol_1 i32 -2013230943
   }
   owi: [ERROR] Reached problem!
   [13]