Explore failed assert first

src/symbolic/symbolic_choice.ml

@@ -366,7 +366,7 @@ let get_model_or_stop symbol =
     | Some v -> return v
   end
 
-let select (cond : Symbolic_value.vbool) =
+let select_inner ?(explore_first = true) (cond : Symbolic_value.vbool) =
   let v = Smtml.Expr.simplify cond in
   match Smtml.Expr.view v with
   | Val True -> return true
@@ -385,9 +385,12 @@ let select (cond : Symbolic_value.vbool) =
       let+ () = check_reachability in
       false
     in
-    choose true_branch false_branch
+    if explore_first then choose true_branch false_branch
+    else choose false_branch true_branch
 [@@inline]
 
+let select (cond : Symbolic_value.vbool) = select_inner cond
+
 let summary_symbol (e : Smtml.Expr.t) =
   let* thread in
   match Smtml.Expr.view e with
@@ -440,7 +443,7 @@ let select_i32 (i : Symbolic_value.int32) =
     generator ()
 
 let assertion c =
-  let* assertion_true = select c in
+  let* assertion_true = select_inner c ~explore_first:false in
   if assertion_true then return ()
   else
     let* thread in