src/cmd/cmd_conc.ml

@@ -541,13 +541,31 @@ let find_model_to_run solver tree =
   | Some pc -> pc_model solver pc
 
 let launch solver tree link_state modules_to_run =
-  let rec loop () =
-    let model = find_model_to_run solver tree in
-    run_model model
-  and run_model model =
+  let rec find_model n =
+    if n = 0 then begin
+      Format.pp_std "Failed to find something to run@\n";
+      None
+    end
+    else
+      match find_model_to_run solver tree with
+      | None -> find_model (n - 1)
+      | Some m ->
+        if debug then begin
+          Format.pp_std "Found something to run %a@\n"
+            (Smtml.Model.pp ~no_values:false)
+            m
+        end;
+        Some m
+  in
+  let rec loop count =
+    if count <= 0 then None
+    else
+      let model = find_model 20 in
+      run_model model count
+  and run_model model count =
     let r, thread = run_once tree link_state modules_to_run model in
     match r with
-    | Ok (Ok ()) -> loop ()
+    | Ok (Ok ()) -> loop (count - 1)
     | Ok (Error e) -> Result.failwith e
     | Error (Assume_fail c) -> begin
       if debug then begin
@@ -559,13 +577,13 @@ let launch solver tree link_state modules_to_run =
       match pc_model solver thread.pc with
       | None ->
         Format.pp_err "Can't satisfy assume !@\n";
-        loop ()
-      | Some _model as model -> run_model model
+        loop (count - 1)
+      | Some _model as model -> run_model model (count - 1)
     end
     | Error (Trap trap) -> Some (`Trap trap, thread)
     | Error Assert_fail -> Some (`Assert_fail, thread)
   in
-  loop ()
+  loop 10
 
 (* NB: This function propagates potential errors (Result.err) occurring
    during evaluation (OS, syntax error, etc.), except for Trap and Assert,