From 28f1ab269ece109ef9c05cec302f72f90371ee16 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 7 May 2021 10:00:36 +0200
Subject: [PATCH] Add option --show-steps
---
src_colibri2/bin/main.ml | 3 +-
src_colibri2/bin/options.ml | 13 ++--
src_colibri2/solver/input.ml | 12 ++--
src_colibri2/solver/scheduler.ml | 19 ++++--
src_colibri2/solver/scheduler.mli | 1 +
.../generate_tests/generate_dune_tests.ml | 2 +-
.../tests/solve/all/steplimitreached/dune.inc | 2 +-
src_colibri2/tests/solve/all/unsat/dune.inc | 4 +-
src_colibri2/tests/solve/dimacs/sat/dune.inc | 22 +++----
.../tests/solve/dimacs/unsat/dune.inc | 12 ++--
src_colibri2/tests/solve/smt_adt/sat/dune.inc | 12 ++--
.../tests/solve/smt_adt/unsat/dune.inc | 16 ++---
src_colibri2/tests/solve/smt_lra/sat/dune.inc | 66 +++++++++----------
.../tests/solve/smt_lra/unsat/dune.inc | 22 +++----
src_colibri2/tests/solve/smt_nra/sat/dune.inc | 14 ++--
.../tests/solve/smt_nra/unsat/dune.inc | 20 +++---
.../tests/solve/smt_quant/sat/dune.inc | 8 +--
.../tests/solve/smt_quant/unsat/dune.inc | 22 +++----
src_colibri2/tests/solve/smt_uf/sat/dune.inc | 42 ++++++------
.../tests/solve/smt_uf/unsat/dune.inc | 26 ++++----
20 files changed, 177 insertions(+), 161 deletions(-)
diff --git a/src_colibri2/bin/main.ml b/src_colibri2/bin/main.ml
index 457225cbf..eda40704f 100644
--- a/src_colibri2/bin/main.ml
+++ b/src_colibri2/bin/main.ml
@@ -33,13 +33,14 @@ let () =
] in
let info = Cmdliner.Term.info ~man ~version:"0.1" "dolmen" in
let theories = Colibri2_core.Egraph.default_theories () in
- let st,step_limit = match Cmdliner.Term.eval (Options.state theories, info) with
+ let st,step_limit,show_steps = match Cmdliner.Term.eval (Options.state theories, info) with
| `Version | `Help -> exit 0
| `Error `Parse | `Error `Term | `Error `Exn -> exit 2
| `Ok opt -> opt
in
Colibri2_solver.Input.read
?limit:step_limit
+ ~show_steps:show_steps
~set_true:Colibri2_theories_bool.Boolean.set_true
~handle_exn:Colibri2_solver.Input.handle_exn_with_exit
st
diff --git a/src_colibri2/bin/options.ml b/src_colibri2/bin/options.ml
index f2c54316a..fef5754cb 100644
--- a/src_colibri2/bin/options.ml
+++ b/src_colibri2/bin/options.ml
@@ -51,7 +51,7 @@ let mk_state theories
header_lang_version
type_check type_strict
debug context max_warn step_limit
- debug_flags
+ debug_flags show_steps
=
List.iter Colibri2_popop_lib.Debug.(fun s -> set_flag (lookup_flag s)) debug_flags;
if debug then
@@ -62,7 +62,7 @@ let mk_state theories
~size_limit ?input_lang ?input_mode ~input
~header_check ~header_licenses ~header_lang_version
~type_check ~type_strict
- ~debug ~context ~max_warn theories, step_limit
+ ~debug ~context ~max_warn theories, step_limit, show_steps
(* Input source converter *)
(* ************************************************************************* *)
@@ -311,7 +311,12 @@ let state theories =
let step_limit =
let doc = Format.asprintf
"Maximum number of steps." in
- Arg.(value & opt (some int) None & info ["max-step"] ~docs ~doc)
+ Arg.(value & opt (some int) None & info ["max-steps"] ~docs ~doc)
+ in
+ let show_steps =
+ let doc = Format.asprintf
+ "Show the number of steps after solving." in
+ Arg.(value & flag & info ["show-steps"] ~docs ~doc)
in
let debug_flags =
let doc = Format.asprintf "Debug flags." in
@@ -320,4 +325,4 @@ let state theories =
Term.(const (mk_state theories) $ gc $ gc_t $ bt $ colors $
time $ size $ in_lang $ in_mode $ input $
header_check $ header_licenses $ header_lang_version $
- typing $ strict $ debug $ context $ max_warn $ step_limit $ debug_flags)
+ typing $ strict $ debug $ context $ max_warn $ step_limit $ debug_flags $ show_steps)
diff --git a/src_colibri2/solver/input.ml b/src_colibri2/solver/input.ml
index dfd18558f..514004502 100644
--- a/src_colibri2/solver/input.ml
+++ b/src_colibri2/solver/input.ml
@@ -227,7 +227,7 @@ let rec pop st i =
pop st (n-1)
-let handle_stmt ?(show_checksat_result=true) ?limit ~set_true (st:State.t) (stmt:Typer.typechecked Typer.stmt) =
+let handle_stmt ?(show_checksat_result=true) ?(show_steps=false) ?limit ~set_true (st:State.t) (stmt:Typer.typechecked Typer.stmt) =
begin match stmt.contents with
| `Reset
| `Get_unsat_core
@@ -251,12 +251,16 @@ let handle_stmt ?(show_checksat_result=true) ?limit ~set_true (st:State.t) (stmt
| `Hyp d -> hyp ~set_true st.State.solve_state d
| `Solve s -> begin
solve ~set_true ?limit st.State.solve_state s;
- if show_checksat_result then
+ if show_checksat_result then begin
match st.State.solve_state.state with
| `Unsat -> Format.printf "unsat@."
| `Sat _ -> Format.printf "sat@."
| `Unknown -> Format.printf "unknown@."
| `StepLimitReached -> Format.printf "steplimitreached@."
+ end;
+ if show_steps then begin
+ Format.printf "(steps %i)@." (Scheduler.get_steps st.State.solve_state.scheduler)
+ end
end
| `Echo s -> Format.printf "%s@." s
| `Set_info _ -> ()
@@ -265,7 +269,7 @@ let handle_stmt ?(show_checksat_result=true) ?limit ~set_true (st:State.t) (stmt
end;
st, ()
-let read ?show_checksat_result ?limit ~set_true ~handle_exn st =
+let read ?show_checksat_result ?show_steps ?limit ~set_true ~handle_exn st =
let st, g =
try Parser.parse [] st
with exn ->
@@ -279,7 +283,7 @@ let read ?show_checksat_result ?limit ~set_true ~handle_exn st =
(op ~name:"debug" debug_pipe)
@>>> (op ~name:"headers" Header.inspect)
@>>> (op ~name:"typecheck" Typer.typecheck)
- @>|> (op (handle_stmt ?show_checksat_result ?limit ~set_true)) @>>> _end
+ @>|> (op (handle_stmt ?show_checksat_result ?show_steps ?limit ~set_true)) @>>> _end
)
)
)
diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index b64924637..f596b2303 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/src_colibri2/solver/scheduler.ml
@@ -90,6 +90,7 @@ type t =
context : Context.context;
mutable level: int;
solve_step: solve_step Context.Ref.t;
+ mutable steps: int;
}
(** To treat in the reverse order *)
@@ -99,6 +100,8 @@ let print_level fmt t =
0 t.choices in
Format.fprintf fmt "%i (dec waiting:%i)" t.level nb_dec
+let get_steps t = t.steps
+
(* let new_handler t =
* if t.delayed <> None then raise NeedStopDelayed;
* {wakeup_daemons = t.wakeup_daemons;
@@ -126,6 +129,7 @@ let new_solver () =
var_inc = ref 1.;
level = 0;
solve_step = Context.Ref.create (Context.creator context) (Propagate);
+ steps = 0;
}
in
let sched_daemon att =
@@ -353,6 +357,7 @@ let run_one_step_fix_model t =
)
let run_one_step ~nodec t =
+ t.steps <- t.steps + 1;
match Context.Ref.get t.solve_step with
| Propagate -> begin
match run_one_step_propagation ~nodec t with
@@ -375,21 +380,21 @@ let rec flush t =
exception ReachStepLimit
-let rec run_inf_step ?limit ~nodec t =
- (match limit with | Some n when n <= 0 -> raise ReachStepLimit | _ -> ());
+let rec run_inf_step ~limit ~nodec t =
+ if t.steps = limit then raise ReachStepLimit;
flush t;
match run_one_step ~nodec t with
| true ->
- run_inf_step ?limit:(Opt.map pred limit) ~nodec t
+ run_inf_step ~limit ~nodec t
| false ->
Egraph.Backtrackable.delayed_stop t.solver_state
-let run_inf_step ?limit ?(nodec=false) t =
+let run_inf_step ?(limit=(-1)) ?(nodec=false) t =
try
- run_inf_step ?limit ~nodec t;
- Debug.dprintf0 debug_pushpop "[Scheduler] sat";
+ run_inf_step ~limit ~nodec t;
+ Debug.dprintf1 debug_pushpop "[Scheduler] sat(%i)" t.steps
with (Contradiction as e) ->
- Debug.dprintf0 debug_pushpop "[Scheduler] unsat";
+ Debug.dprintf1 debug_pushpop "[Scheduler] unsat(%i)" t.steps;
raise e
let init_theories ~theories t =
diff --git a/src_colibri2/solver/scheduler.mli b/src_colibri2/solver/scheduler.mli
index d4c7ee4ea..272e1651b 100644
--- a/src_colibri2/solver/scheduler.mli
+++ b/src_colibri2/solver/scheduler.mli
@@ -41,6 +41,7 @@ val new_solver: unit -> t
val init_theories: theories:(Egraph.t -> unit) list -> t -> unit
val add_assertion: t -> (Egraph.t -> unit) -> unit
val check_sat: ?limit:int -> t -> [> `Unsat | `Sat of Egraph.t ]
+val get_steps: t -> int
type bp
diff --git a/src_colibri2/tests/generate_tests/generate_dune_tests.ml b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
index 7094b142d..6c2442232 100644
--- a/src_colibri2/tests/generate_tests/generate_dune_tests.ml
+++ b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
@@ -23,7 +23,7 @@ let result = Sys.argv.(2)
let print_test cout file =
Printf.fprintf cout
- "(rule (action (with-stdout-to %s.res (run %%{bin:colibri2} --max-step 3000 %%{dep:%s}))))\n"
+ "(rule (action (with-stdout-to %s.res (run %%{bin:colibri2} --max-steps 3000 %%{dep:%s}))))\n"
file file;
Printf.fprintf cout
"(rule (alias runtest) (action (diff oracle %s.res)))\n"
diff --git a/src_colibri2/tests/solve/all/steplimitreached/dune.inc b/src_colibri2/tests/solve/all/steplimitreached/dune.inc
index 7a7c228ca..48f937957 100644
--- a/src_colibri2/tests/solve/all/steplimitreached/dune.inc
+++ b/src_colibri2/tests/solve/all/steplimitreached/dune.inc
@@ -1,3 +1,3 @@
(rule (action (with-stdout-to oracle (echo "steplimitreached\n"))))
-(rule (action (with-stdout-to bag-BagImpl-addqtvc.psmt2.res (run %{bin:colibri2} --max-step 3000 %{dep:bag-BagImpl-addqtvc.psmt2}))))
+(rule (action (with-stdout-to bag-BagImpl-addqtvc.psmt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:bag-BagImpl-addqtvc.psmt2}))))
(rule (alias runtest) (action (diff oracle bag-BagImpl-addqtvc.psmt2.res)))
diff --git a/src_colibri2/tests/solve/all/unsat/dune.inc b/src_colibri2/tests/solve/all/unsat/dune.inc
index 5120eabbe..ecab8ff93 100644
--- a/src_colibri2/tests/solve/all/unsat/dune.inc
+++ b/src_colibri2/tests/solve/all/unsat/dune.inc
@@ -1,5 +1,5 @@
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to bag-BagImpl-createqtvc.psmt2.res (run %{bin:colibri2} --max-step 3000 %{dep:bag-BagImpl-createqtvc.psmt2}))))
+(rule (action (with-stdout-to bag-BagImpl-createqtvc.psmt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:bag-BagImpl-createqtvc.psmt2}))))
(rule (alias runtest) (action (diff oracle bag-BagImpl-createqtvc.psmt2.res)))
-(rule (action (with-stdout-to fact-FactRecursive-fact_recqtvc.psmt2.res (run %{bin:colibri2} --max-step 3000 %{dep:fact-FactRecursive-fact_recqtvc.psmt2}))))
+(rule (action (with-stdout-to fact-FactRecursive-fact_recqtvc.psmt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:fact-FactRecursive-fact_recqtvc.psmt2}))))
(rule (alias runtest) (action (diff oracle fact-FactRecursive-fact_recqtvc.psmt2.res)))
diff --git a/src_colibri2/tests/solve/dimacs/sat/dune.inc b/src_colibri2/tests/solve/dimacs/sat/dune.inc
index a3f62fc4b..578b32831 100644
--- a/src_colibri2/tests/solve/dimacs/sat/dune.inc
+++ b/src_colibri2/tests/solve/dimacs/sat/dune.inc
@@ -1,23 +1,23 @@
(rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:anomaly_agetooold.cnf}))))
+(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:anomaly_agetooold.cnf}))))
(rule (alias runtest) (action (diff oracle anomaly_agetooold.cnf.res)))
-(rule (action (with-stdout-to anomaly_agetooold2.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:anomaly_agetooold2.cnf}))))
+(rule (action (with-stdout-to anomaly_agetooold2.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:anomaly_agetooold2.cnf}))))
(rule (alias runtest) (action (diff oracle anomaly_agetooold2.cnf.res)))
-(rule (action (with-stdout-to assertion_fail.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:assertion_fail.cnf}))))
+(rule (action (with-stdout-to assertion_fail.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:assertion_fail.cnf}))))
(rule (alias runtest) (action (diff oracle assertion_fail.cnf.res)))
-(rule (action (with-stdout-to fuzzing1.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:fuzzing1.cnf}))))
+(rule (action (with-stdout-to fuzzing1.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:fuzzing1.cnf}))))
(rule (alias runtest) (action (diff oracle fuzzing1.cnf.res)))
-(rule (action (with-stdout-to fuzzing2.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:fuzzing2.cnf}))))
+(rule (action (with-stdout-to fuzzing2.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:fuzzing2.cnf}))))
(rule (alias runtest) (action (diff oracle fuzzing2.cnf.res)))
-(rule (action (with-stdout-to par8-1-c.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:par8-1-c.cnf}))))
+(rule (action (with-stdout-to par8-1-c.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:par8-1-c.cnf}))))
(rule (alias runtest) (action (diff oracle par8-1-c.cnf.res)))
-(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-2.cnf}))))
+(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:pigeon-2.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-2.cnf.res)))
-(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-3.cnf}))))
+(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:pigeon-3.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-3.cnf.res)))
-(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-4.cnf}))))
+(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:pigeon-4.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-4.cnf.res)))
-(rule (action (with-stdout-to quinn.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:quinn.cnf}))))
+(rule (action (with-stdout-to quinn.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:quinn.cnf}))))
(rule (alias runtest) (action (diff oracle quinn.cnf.res)))
-(rule (action (with-stdout-to simple_v3_c2.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:simple_v3_c2.cnf}))))
+(rule (action (with-stdout-to simple_v3_c2.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:simple_v3_c2.cnf}))))
(rule (alias runtest) (action (diff oracle simple_v3_c2.cnf.res)))
diff --git a/src_colibri2/tests/solve/dimacs/unsat/dune.inc b/src_colibri2/tests/solve/dimacs/unsat/dune.inc
index 5766ddefe..cb881c555 100644
--- a/src_colibri2/tests/solve/dimacs/unsat/dune.inc
+++ b/src_colibri2/tests/solve/dimacs/unsat/dune.inc
@@ -1,13 +1,13 @@
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:anomaly_agetooold.cnf}))))
+(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:anomaly_agetooold.cnf}))))
(rule (alias runtest) (action (diff oracle anomaly_agetooold.cnf.res)))
-(rule (action (with-stdout-to modus_ponens.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:modus_ponens.cnf}))))
+(rule (action (with-stdout-to modus_ponens.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:modus_ponens.cnf}))))
(rule (alias runtest) (action (diff oracle modus_ponens.cnf.res)))
-(rule (action (with-stdout-to pigeon-1.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-1.cnf}))))
+(rule (action (with-stdout-to pigeon-1.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:pigeon-1.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-1.cnf.res)))
-(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-2.cnf}))))
+(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:pigeon-2.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-2.cnf.res)))
-(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-3.cnf}))))
+(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:pigeon-3.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-3.cnf.res)))
-(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-4.cnf}))))
+(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:pigeon-4.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-4.cnf.res)))
diff --git a/src_colibri2/tests/solve/smt_adt/sat/dune.inc b/src_colibri2/tests/solve/smt_adt/sat/dune.inc
index 38973a521..93d4bd675 100644
--- a/src_colibri2/tests/solve/smt_adt/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_adt/sat/dune.inc
@@ -1,13 +1,13 @@
(rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:enum.smt2}))))
+(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:enum.smt2}))))
(rule (alias runtest) (action (diff oracle enum.smt2.res)))
-(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list0.smt2}))))
+(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:list0.smt2}))))
(rule (alias runtest) (action (diff oracle list0.smt2.res)))
-(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list1.smt2}))))
+(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:list1.smt2}))))
(rule (alias runtest) (action (diff oracle list1.smt2.res)))
-(rule (action (with-stdout-to tree1.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:tree1.smt2}))))
+(rule (action (with-stdout-to tree1.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:tree1.smt2}))))
(rule (alias runtest) (action (diff oracle tree1.smt2.res)))
-(rule (action (with-stdout-to tree2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:tree2.smt2}))))
+(rule (action (with-stdout-to tree2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:tree2.smt2}))))
(rule (alias runtest) (action (diff oracle tree2.smt2.res)))
-(rule (action (with-stdout-to tree3.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:tree3.smt2}))))
+(rule (action (with-stdout-to tree3.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:tree3.smt2}))))
(rule (alias runtest) (action (diff oracle tree3.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_adt/unsat/dune.inc b/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
index 55451ca3a..a8533a278 100644
--- a/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
@@ -1,17 +1,17 @@
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:enum.smt2}))))
+(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:enum.smt2}))))
(rule (alias runtest) (action (diff oracle enum.smt2.res)))
-(rule (action (with-stdout-to enum2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:enum2.smt2}))))
+(rule (action (with-stdout-to enum2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:enum2.smt2}))))
(rule (alias runtest) (action (diff oracle enum2.smt2.res)))
-(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list0.smt2}))))
+(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:list0.smt2}))))
(rule (alias runtest) (action (diff oracle list0.smt2.res)))
-(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list1.smt2}))))
+(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:list1.smt2}))))
(rule (alias runtest) (action (diff oracle list1.smt2.res)))
-(rule (action (with-stdout-to list2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list2.smt2}))))
+(rule (action (with-stdout-to list2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:list2.smt2}))))
(rule (alias runtest) (action (diff oracle list2.smt2.res)))
-(rule (action (with-stdout-to list3.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list3.smt2}))))
+(rule (action (with-stdout-to list3.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:list3.smt2}))))
(rule (alias runtest) (action (diff oracle list3.smt2.res)))
-(rule (action (with-stdout-to list4.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list4.smt2}))))
+(rule (action (with-stdout-to list4.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:list4.smt2}))))
(rule (alias runtest) (action (diff oracle list4.smt2.res)))
-(rule (action (with-stdout-to parlist0.psmt2.res (run %{bin:colibri2} --max-step 3000 %{dep:parlist0.psmt2}))))
+(rule (action (with-stdout-to parlist0.psmt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:parlist0.psmt2}))))
(rule (alias runtest) (action (diff oracle parlist0.psmt2.res)))
diff --git a/src_colibri2/tests/solve/smt_lra/sat/dune.inc b/src_colibri2/tests/solve/smt_lra/sat/dune.inc
index b5a74a06e..20107a851 100644
--- a/src_colibri2/tests/solve/smt_lra/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_lra/sat/dune.inc
@@ -1,67 +1,67 @@
(rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to arith_CombiRepr_normalize.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_CombiRepr_normalize.smt2}))))
+(rule (action (with-stdout-to arith_CombiRepr_normalize.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_CombiRepr_normalize.smt2}))))
(rule (alias runtest) (action (diff oracle arith_CombiRepr_normalize.smt2.res)))
-(rule (action (with-stdout-to arith_conflict_add_disequality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_conflict_add_disequality.smt2}))))
+(rule (action (with-stdout-to arith_conflict_add_disequality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_conflict_add_disequality.smt2}))))
(rule (alias runtest) (action (diff oracle arith_conflict_add_disequality.smt2.res)))
-(rule (action (with-stdout-to arith_conpoly.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_conpoly.smt2}))))
+(rule (action (with-stdout-to arith_conpoly.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_conpoly.smt2}))))
(rule (alias runtest) (action (diff oracle arith_conpoly.smt2.res)))
-(rule (action (with-stdout-to arith_decide_must_test_is_dis_equal.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_decide_must_test_is_dis_equal.smt2}))))
+(rule (action (with-stdout-to arith_decide_must_test_is_dis_equal.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_decide_must_test_is_dis_equal.smt2}))))
(rule (alias runtest) (action (diff oracle arith_decide_must_test_is_dis_equal.smt2.res)))
-(rule (action (with-stdout-to arith_init_always_merge_itself.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_init_always_merge_itself.smt2}))))
+(rule (action (with-stdout-to arith_init_always_merge_itself.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_init_always_merge_itself.smt2}))))
(rule (alias runtest) (action (diff oracle arith_init_always_merge_itself.smt2.res)))
-(rule (action (with-stdout-to arith_init_and_propa_must_be_ordered.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_init_and_propa_must_be_ordered.smt2}))))
+(rule (action (with-stdout-to arith_init_and_propa_must_be_ordered.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_init_and_propa_must_be_ordered.smt2}))))
(rule (alias runtest) (action (diff oracle arith_init_and_propa_must_be_ordered.smt2.res)))
-(rule (action (with-stdout-to arith_merge_case1.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_case1.smt2}))))
+(rule (action (with-stdout-to arith_merge_case1.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_case1.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_case1.smt2.res)))
-(rule (action (with-stdout-to arith_merge_case_4.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_case_4.smt2}))))
+(rule (action (with-stdout-to arith_merge_case_4.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_case_4.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_case_4.smt2.res)))
-(rule (action (with-stdout-to arith_merge_case_4_bis.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_case_4_bis.smt2}))))
+(rule (action (with-stdout-to arith_merge_case_4_bis.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_case_4_bis.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_case_4_bis.smt2.res)))
-(rule (action (with-stdout-to arith_merge_itself_coef_of_repr_is_one.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_itself_coef_of_repr_is_one.smt2}))))
+(rule (action (with-stdout-to arith_merge_itself_coef_of_repr_is_one.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_itself_coef_of_repr_is_one.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_itself_coef_of_repr_is_one.smt2.res)))
-(rule (action (with-stdout-to arith_merge_itself_last_case.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_itself_last_case.smt2}))))
+(rule (action (with-stdout-to arith_merge_itself_last_case.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_itself_last_case.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_itself_last_case.smt2.res)))
-(rule (action (with-stdout-to arith_merge_itself_pivot_not_in_p12.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_itself_pivot_not_in_p12.smt2}))))
+(rule (action (with-stdout-to arith_merge_itself_pivot_not_in_p12.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_itself_pivot_not_in_p12.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_itself_pivot_not_in_p12.smt2.res)))
-(rule (action (with-stdout-to arith_merge_must_use_find.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_must_use_find.smt2}))))
+(rule (action (with-stdout-to arith_merge_must_use_find.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_must_use_find.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_must_use_find.smt2.res)))
-(rule (action (with-stdout-to arith_mult_explication.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_mult_explication.smt2}))))
+(rule (action (with-stdout-to arith_mult_explication.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_mult_explication.smt2}))))
(rule (alias runtest) (action (diff oracle arith_mult_explication.smt2.res)))
-(rule (action (with-stdout-to arith_mult_not_linear_in_conflict.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_mult_not_linear_in_conflict.smt2}))))
+(rule (action (with-stdout-to arith_mult_not_linear_in_conflict.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_mult_not_linear_in_conflict.smt2}))))
(rule (alias runtest) (action (diff oracle arith_mult_not_linear_in_conflict.smt2.res)))
-(rule (action (with-stdout-to arith_normalize_use_find_def.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_normalize_use_find_def.smt2}))))
+(rule (action (with-stdout-to arith_normalize_use_find_def.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_normalize_use_find_def.smt2}))))
(rule (alias runtest) (action (diff oracle arith_normalize_use_find_def.smt2.res)))
-(rule (action (with-stdout-to arith_own_repr.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_own_repr.smt2}))))
+(rule (action (with-stdout-to arith_own_repr.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_own_repr.smt2}))))
(rule (alias runtest) (action (diff oracle arith_own_repr.smt2.res)))
-(rule (action (with-stdout-to arith_propacl.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_propacl.smt2}))))
+(rule (action (with-stdout-to arith_propacl.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_propacl.smt2}))))
(rule (alias runtest) (action (diff oracle arith_propacl.smt2.res)))
-(rule (action (with-stdout-to arith_subst_and_conflict_add.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_subst_and_conflict_add.smt2}))))
+(rule (action (with-stdout-to arith_subst_and_conflict_add.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_subst_and_conflict_add.smt2}))))
(rule (alias runtest) (action (diff oracle arith_subst_and_conflict_add.smt2.res)))
-(rule (action (with-stdout-to arith_zero_dom.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_zero_dom.smt2}))))
+(rule (action (with-stdout-to arith_zero_dom.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_zero_dom.smt2}))))
(rule (alias runtest) (action (diff oracle arith_zero_dom.smt2.res)))
-(rule (action (with-stdout-to attach_only_when_dom_present.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:attach_only_when_dom_present.smt2}))))
+(rule (action (with-stdout-to attach_only_when_dom_present.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:attach_only_when_dom_present.smt2}))))
(rule (alias runtest) (action (diff oracle attach_only_when_dom_present.smt2.res)))
-(rule (action (with-stdout-to init_not_repr.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:init_not_repr.smt2}))))
+(rule (action (with-stdout-to init_not_repr.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:init_not_repr.smt2}))))
(rule (alias runtest) (action (diff oracle init_not_repr.smt2.res)))
-(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:le.smt2}))))
+(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:le.smt2}))))
(rule (alias runtest) (action (diff oracle le.smt2.res)))
-(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:le2.smt2}))))
+(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:le2.smt2}))))
(rule (alias runtest) (action (diff oracle le2.smt2.res)))
-(rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul.smt2}))))
+(rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul.smt2}))))
(rule (alias runtest) (action (diff oracle mul.smt2.res)))
-(rule (action (with-stdout-to sem_invariant_in_learnt_dec.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:sem_invariant_in_learnt_dec.smt2}))))
+(rule (action (with-stdout-to sem_invariant_in_learnt_dec.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:sem_invariant_in_learnt_dec.smt2}))))
(rule (alias runtest) (action (diff oracle sem_invariant_in_learnt_dec.smt2.res)))
-(rule (action (with-stdout-to solver_add_pexp_cl.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_add_pexp_cl.smt2}))))
+(rule (action (with-stdout-to solver_add_pexp_cl.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:solver_add_pexp_cl.smt2}))))
(rule (alias runtest) (action (diff oracle solver_add_pexp_cl.smt2.res)))
-(rule (action (with-stdout-to solver_arith_homogeneous_dist_sign.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_arith_homogeneous_dist_sign.smt2}))))
+(rule (action (with-stdout-to solver_arith_homogeneous_dist_sign.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:solver_arith_homogeneous_dist_sign.smt2}))))
(rule (alias runtest) (action (diff oracle solver_arith_homogeneous_dist_sign.smt2.res)))
-(rule (action (with-stdout-to solver_merge_itself_repr_inside.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_merge_itself_repr_inside.smt2}))))
+(rule (action (with-stdout-to solver_merge_itself_repr_inside.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:solver_merge_itself_repr_inside.smt2}))))
(rule (alias runtest) (action (diff oracle solver_merge_itself_repr_inside.smt2.res)))
-(rule (action (with-stdout-to solver_set_pending_merge_expsameexp.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_set_pending_merge_expsameexp.smt2}))))
+(rule (action (with-stdout-to solver_set_pending_merge_expsameexp.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:solver_set_pending_merge_expsameexp.smt2}))))
(rule (alias runtest) (action (diff oracle solver_set_pending_merge_expsameexp.smt2.res)))
-(rule (action (with-stdout-to solver_subst_eventdom_find.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_subst_eventdom_find.smt2}))))
+(rule (action (with-stdout-to solver_subst_eventdom_find.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:solver_subst_eventdom_find.smt2}))))
(rule (alias runtest) (action (diff oracle solver_subst_eventdom_find.smt2.res)))
-(rule (action (with-stdout-to to_real.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:to_real.smt2}))))
+(rule (action (with-stdout-to to_real.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:to_real.smt2}))))
(rule (alias runtest) (action (diff oracle to_real.smt2.res)))
-(rule (action (with-stdout-to to_real2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:to_real2.smt2}))))
+(rule (action (with-stdout-to to_real2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:to_real2.smt2}))))
(rule (alias runtest) (action (diff oracle to_real2.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_lra/unsat/dune.inc b/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
index 7247c5c7a..419d393cf 100644
--- a/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
@@ -1,23 +1,23 @@
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to arith_ExpMult_by_zero.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_ExpMult_by_zero.smt2}))))
+(rule (action (with-stdout-to arith_ExpMult_by_zero.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_ExpMult_by_zero.smt2}))))
(rule (alias runtest) (action (diff oracle arith_ExpMult_by_zero.smt2.res)))
-(rule (action (with-stdout-to arith_merge_case2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_case2.smt2}))))
+(rule (action (with-stdout-to arith_merge_case2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_case2.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_case2.smt2.res)))
-(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:le.smt2}))))
+(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:le.smt2}))))
(rule (alias runtest) (action (diff oracle le.smt2.res)))
-(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:le2.smt2}))))
+(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:le2.smt2}))))
(rule (alias runtest) (action (diff oracle le2.smt2.res)))
-(rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul.smt2}))))
+(rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul.smt2}))))
(rule (alias runtest) (action (diff oracle mul.smt2.res)))
-(rule (action (with-stdout-to repr_and_poly.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:repr_and_poly.smt2}))))
+(rule (action (with-stdout-to repr_and_poly.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:repr_and_poly.smt2}))))
(rule (alias runtest) (action (diff oracle repr_and_poly.smt2.res)))
-(rule (action (with-stdout-to repr_fourier.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:repr_fourier.smt2}))))
+(rule (action (with-stdout-to repr_fourier.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:repr_fourier.smt2}))))
(rule (alias runtest) (action (diff oracle repr_fourier.smt2.res)))
-(rule (action (with-stdout-to solver_merge_itself_repr_empty.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_merge_itself_repr_empty.smt2}))))
+(rule (action (with-stdout-to solver_merge_itself_repr_empty.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:solver_merge_itself_repr_empty.smt2}))))
(rule (alias runtest) (action (diff oracle solver_merge_itself_repr_empty.smt2.res)))
-(rule (action (with-stdout-to solver_set_sem_merge_sign.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_set_sem_merge_sign.smt2}))))
+(rule (action (with-stdout-to solver_set_sem_merge_sign.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:solver_set_sem_merge_sign.smt2}))))
(rule (alias runtest) (action (diff oracle solver_set_sem_merge_sign.smt2.res)))
-(rule (action (with-stdout-to to_real.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:to_real.smt2}))))
+(rule (action (with-stdout-to to_real.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:to_real.smt2}))))
(rule (alias runtest) (action (diff oracle to_real.smt2.res)))
-(rule (action (with-stdout-to to_real2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:to_real2.smt2}))))
+(rule (action (with-stdout-to to_real2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:to_real2.smt2}))))
(rule (alias runtest) (action (diff oracle to_real2.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_nra/sat/dune.inc b/src_colibri2/tests/solve/smt_nra/sat/dune.inc
index 4933b571d..9904173a9 100644
--- a/src_colibri2/tests/solve/smt_nra/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_nra/sat/dune.inc
@@ -1,15 +1,15 @@
(rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to ceil.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:ceil.smt2}))))
+(rule (action (with-stdout-to ceil.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:ceil.smt2}))))
(rule (alias runtest) (action (diff oracle ceil.smt2.res)))
-(rule (action (with-stdout-to div_pos.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:div_pos.smt2}))))
+(rule (action (with-stdout-to div_pos.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:div_pos.smt2}))))
(rule (alias runtest) (action (diff oracle div_pos.smt2.res)))
-(rule (action (with-stdout-to div_pos_lt.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:div_pos_lt.smt2}))))
+(rule (action (with-stdout-to div_pos_lt.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:div_pos_lt.smt2}))))
(rule (alias runtest) (action (diff oracle div_pos_lt.smt2.res)))
-(rule (action (with-stdout-to mul_commut.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_commut.smt2}))))
+(rule (action (with-stdout-to mul_commut.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_commut.smt2}))))
(rule (alias runtest) (action (diff oracle mul_commut.smt2.res)))
-(rule (action (with-stdout-to mul_commut2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_commut2.smt2}))))
+(rule (action (with-stdout-to mul_commut2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_commut2.smt2}))))
(rule (alias runtest) (action (diff oracle mul_commut2.smt2.res)))
-(rule (action (with-stdout-to mul_pos.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_pos.smt2}))))
+(rule (action (with-stdout-to mul_pos.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_pos.smt2}))))
(rule (alias runtest) (action (diff oracle mul_pos.smt2.res)))
-(rule (action (with-stdout-to mul_pos_lt.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_pos_lt.smt2}))))
+(rule (action (with-stdout-to mul_pos_lt.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_pos_lt.smt2}))))
(rule (alias runtest) (action (diff oracle mul_pos_lt.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_nra/unsat/dune.inc b/src_colibri2/tests/solve/smt_nra/unsat/dune.inc
index 3910cff2d..483f0dfcc 100644
--- a/src_colibri2/tests/solve/smt_nra/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_nra/unsat/dune.inc
@@ -1,21 +1,21 @@
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to ceil.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:ceil.smt2}))))
+(rule (action (with-stdout-to ceil.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:ceil.smt2}))))
(rule (alias runtest) (action (diff oracle ceil.smt2.res)))
-(rule (action (with-stdout-to div_pos.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:div_pos.smt2}))))
+(rule (action (with-stdout-to div_pos.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:div_pos.smt2}))))
(rule (alias runtest) (action (diff oracle div_pos.smt2.res)))
-(rule (action (with-stdout-to div_pos_lt.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:div_pos_lt.smt2}))))
+(rule (action (with-stdout-to div_pos_lt.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:div_pos_lt.smt2}))))
(rule (alias runtest) (action (diff oracle div_pos_lt.smt2.res)))
-(rule (action (with-stdout-to div_pos_lt_to_real.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:div_pos_lt_to_real.smt2}))))
+(rule (action (with-stdout-to div_pos_lt_to_real.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:div_pos_lt_to_real.smt2}))))
(rule (alias runtest) (action (diff oracle div_pos_lt_to_real.smt2.res)))
-(rule (action (with-stdout-to floor.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:floor.smt2}))))
+(rule (action (with-stdout-to floor.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:floor.smt2}))))
(rule (alias runtest) (action (diff oracle floor.smt2.res)))
-(rule (action (with-stdout-to mul_commut.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_commut.smt2}))))
+(rule (action (with-stdout-to mul_commut.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_commut.smt2}))))
(rule (alias runtest) (action (diff oracle mul_commut.smt2.res)))
-(rule (action (with-stdout-to mul_commut2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_commut2.smt2}))))
+(rule (action (with-stdout-to mul_commut2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_commut2.smt2}))))
(rule (alias runtest) (action (diff oracle mul_commut2.smt2.res)))
-(rule (action (with-stdout-to mul_pos.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_pos.smt2}))))
+(rule (action (with-stdout-to mul_pos.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_pos.smt2}))))
(rule (alias runtest) (action (diff oracle mul_pos.smt2.res)))
-(rule (action (with-stdout-to mul_pos_lt.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_pos_lt.smt2}))))
+(rule (action (with-stdout-to mul_pos_lt.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_pos_lt.smt2}))))
(rule (alias runtest) (action (diff oracle mul_pos_lt.smt2.res)))
-(rule (action (with-stdout-to mul_pos_zero_le.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_pos_zero_le.smt2}))))
+(rule (action (with-stdout-to mul_pos_zero_le.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_pos_zero_le.smt2}))))
(rule (alias runtest) (action (diff oracle mul_pos_zero_le.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_quant/sat/dune.inc b/src_colibri2/tests/solve/smt_quant/sat/dune.inc
index cc94dac97..f03644ff1 100644
--- a/src_colibri2/tests/solve/smt_quant/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_quant/sat/dune.inc
@@ -1,9 +1,9 @@
(rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:exists.smt2}))))
+(rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:exists.smt2}))))
(rule (alias runtest) (action (diff oracle exists.smt2.res)))
-(rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall0.smt2}))))
+(rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall0.smt2}))))
(rule (alias runtest) (action (diff oracle forall0.smt2.res)))
-(rule (action (with-stdout-to forall3.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall3.smt2}))))
+(rule (action (with-stdout-to forall3.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall3.smt2}))))
(rule (alias runtest) (action (diff oracle forall3.smt2.res)))
-(rule (action (with-stdout-to forall4.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall4.smt2}))))
+(rule (action (with-stdout-to forall4.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall4.smt2}))))
(rule (alias runtest) (action (diff oracle forall4.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_quant/unsat/dune.inc b/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
index b5b0d9392..9d7e931a8 100644
--- a/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
@@ -1,23 +1,23 @@
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:exists.smt2}))))
+(rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:exists.smt2}))))
(rule (alias runtest) (action (diff oracle exists.smt2.res)))
-(rule (action (with-stdout-to exists2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:exists2.smt2}))))
+(rule (action (with-stdout-to exists2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:exists2.smt2}))))
(rule (alias runtest) (action (diff oracle exists2.smt2.res)))
-(rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall0.smt2}))))
+(rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall0.smt2}))))
(rule (alias runtest) (action (diff oracle forall0.smt2.res)))
-(rule (action (with-stdout-to forall1.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall1.smt2}))))
+(rule (action (with-stdout-to forall1.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall1.smt2}))))
(rule (alias runtest) (action (diff oracle forall1.smt2.res)))
-(rule (action (with-stdout-to forall2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall2.smt2}))))
+(rule (action (with-stdout-to forall2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall2.smt2}))))
(rule (alias runtest) (action (diff oracle forall2.smt2.res)))
-(rule (action (with-stdout-to forall3.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall3.smt2}))))
+(rule (action (with-stdout-to forall3.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall3.smt2}))))
(rule (alias runtest) (action (diff oracle forall3.smt2.res)))
-(rule (action (with-stdout-to forall4.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall4.smt2}))))
+(rule (action (with-stdout-to forall4.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall4.smt2}))))
(rule (alias runtest) (action (diff oracle forall4.smt2.res)))
-(rule (action (with-stdout-to forall5.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall5.smt2}))))
+(rule (action (with-stdout-to forall5.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall5.smt2}))))
(rule (alias runtest) (action (diff oracle forall5.smt2.res)))
-(rule (action (with-stdout-to forall6.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall6.smt2}))))
+(rule (action (with-stdout-to forall6.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall6.smt2}))))
(rule (alias runtest) (action (diff oracle forall6.smt2.res)))
-(rule (action (with-stdout-to forall7.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall7.smt2}))))
+(rule (action (with-stdout-to forall7.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall7.smt2}))))
(rule (alias runtest) (action (diff oracle forall7.smt2.res)))
-(rule (action (with-stdout-to forall8.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall8.smt2}))))
+(rule (action (with-stdout-to forall8.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall8.smt2}))))
(rule (alias runtest) (action (diff oracle forall8.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_uf/sat/dune.inc b/src_colibri2/tests/solve/smt_uf/sat/dune.inc
index d9082d43c..a6b45388b 100644
--- a/src_colibri2/tests/solve/smt_uf/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_uf/sat/dune.inc
@@ -1,43 +1,43 @@
(rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to bad_conflict.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:bad_conflict.smt2}))))
+(rule (action (with-stdout-to bad_conflict.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:bad_conflict.smt2}))))
(rule (alias runtest) (action (diff oracle bad_conflict.smt2.res)))
-(rule (action (with-stdout-to bcp_dont_like_duplicate.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:bcp_dont_like_duplicate.smt2}))))
+(rule (action (with-stdout-to bcp_dont_like_duplicate.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:bcp_dont_like_duplicate.smt2}))))
(rule (alias runtest) (action (diff oracle bcp_dont_like_duplicate.smt2.res)))
-(rule (action (with-stdout-to bool_not_propa.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:bool_not_propa.smt2}))))
+(rule (action (with-stdout-to bool_not_propa.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:bool_not_propa.smt2}))))
(rule (alias runtest) (action (diff oracle bool_not_propa.smt2.res)))
-(rule (action (with-stdout-to boolexpup.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:boolexpup.smt2}))))
+(rule (action (with-stdout-to boolexpup.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:boolexpup.smt2}))))
(rule (alias runtest) (action (diff oracle boolexpup.smt2.res)))
-(rule (action (with-stdout-to clause_normalization.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:clause_normalization.smt2}))))
+(rule (action (with-stdout-to clause_normalization.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:clause_normalization.smt2}))))
(rule (alias runtest) (action (diff oracle clause_normalization.smt2.res)))
-(rule (action (with-stdout-to clmerge.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:clmerge.smt2}))))
+(rule (action (with-stdout-to clmerge.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:clmerge.smt2}))))
(rule (alias runtest) (action (diff oracle clmerge.smt2.res)))
-(rule (action (with-stdout-to conflict_complete_needed_cl.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:conflict_complete_needed_cl.smt2}))))
+(rule (action (with-stdout-to conflict_complete_needed_cl.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:conflict_complete_needed_cl.smt2}))))
(rule (alias runtest) (action (diff oracle conflict_complete_needed_cl.smt2.res)))
-(rule (action (with-stdout-to directdom_not.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:directdom_not.smt2}))))
+(rule (action (with-stdout-to directdom_not.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:directdom_not.smt2}))))
(rule (alias runtest) (action (diff oracle directdom_not.smt2.res)))
-(rule (action (with-stdout-to dis_dom_before_first_age.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:dis_dom_before_first_age.smt2}))))
+(rule (action (with-stdout-to dis_dom_before_first_age.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:dis_dom_before_first_age.smt2}))))
(rule (alias runtest) (action (diff oracle dis_dom_before_first_age.smt2.res)))
-(rule (action (with-stdout-to dom_merge_equality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:dom_merge_equality.smt2}))))
+(rule (action (with-stdout-to dom_merge_equality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:dom_merge_equality.smt2}))))
(rule (alias runtest) (action (diff oracle dom_merge_equality.smt2.res)))
-(rule (action (with-stdout-to equality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:equality.smt2}))))
+(rule (action (with-stdout-to equality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:equality.smt2}))))
(rule (alias runtest) (action (diff oracle equality.smt2.res)))
-(rule (action (with-stdout-to equality_condis.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:equality_condis.smt2}))))
+(rule (action (with-stdout-to equality_condis.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:equality_condis.smt2}))))
(rule (alias runtest) (action (diff oracle equality_condis.smt2.res)))
-(rule (action (with-stdout-to equality_get_sem.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:equality_get_sem.smt2}))))
+(rule (action (with-stdout-to equality_get_sem.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:equality_get_sem.smt2}))))
(rule (alias runtest) (action (diff oracle equality_get_sem.smt2.res)))
-(rule (action (with-stdout-to exp_sem_equality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:exp_sem_equality.smt2}))))
+(rule (action (with-stdout-to exp_sem_equality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:exp_sem_equality.smt2}))))
(rule (alias runtest) (action (diff oracle exp_sem_equality.smt2.res)))
-(rule (action (with-stdout-to explimit_cl_equality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:explimit_cl_equality.smt2}))))
+(rule (action (with-stdout-to explimit_cl_equality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:explimit_cl_equality.smt2}))))
(rule (alias runtest) (action (diff oracle explimit_cl_equality.smt2.res)))
-(rule (action (with-stdout-to implication.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:implication.smt2}))))
+(rule (action (with-stdout-to implication.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:implication.smt2}))))
(rule (alias runtest) (action (diff oracle implication.smt2.res)))
-(rule (action (with-stdout-to intmap_set_disjoint.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:intmap_set_disjoint.smt2}))))
+(rule (action (with-stdout-to intmap_set_disjoint.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:intmap_set_disjoint.smt2}))))
(rule (alias runtest) (action (diff oracle intmap_set_disjoint.smt2.res)))
-(rule (action (with-stdout-to is_equal_not_propagated.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:is_equal_not_propagated.smt2}))))
+(rule (action (with-stdout-to is_equal_not_propagated.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:is_equal_not_propagated.smt2}))))
(rule (alias runtest) (action (diff oracle is_equal_not_propagated.smt2.res)))
-(rule (action (with-stdout-to ite_sem_bool.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:ite_sem_bool.smt2}))))
+(rule (action (with-stdout-to ite_sem_bool.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:ite_sem_bool.smt2}))))
(rule (alias runtest) (action (diff oracle ite_sem_bool.smt2.res)))
-(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:polyeq_genequality.smt2}))))
+(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:polyeq_genequality.smt2}))))
(rule (alias runtest) (action (diff oracle polyeq_genequality.smt2.res)))
-(rule (action (with-stdout-to substupfalse_equality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:substupfalse_equality.smt2}))))
+(rule (action (with-stdout-to substupfalse_equality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:substupfalse_equality.smt2}))))
(rule (alias runtest) (action (diff oracle substupfalse_equality.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_uf/unsat/dune.inc b/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
index 137b8afa1..0b7a4dca9 100644
--- a/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
@@ -1,27 +1,27 @@
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to NEQ004_size4__decide_eq_us.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:NEQ004_size4__decide_eq_us.smt2}))))
+(rule (action (with-stdout-to NEQ004_size4__decide_eq_us.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:NEQ004_size4__decide_eq_us.smt2}))))
(rule (alias runtest) (action (diff oracle NEQ004_size4__decide_eq_us.smt2.res)))
-(rule (action (with-stdout-to deltaed0.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:deltaed0.smt2}))))
+(rule (action (with-stdout-to deltaed0.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:deltaed0.smt2}))))
(rule (alias runtest) (action (diff oracle deltaed0.smt2.res)))
-(rule (action (with-stdout-to diff_to_value_for_bool.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:diff_to_value_for_bool.smt2}))))
+(rule (action (with-stdout-to diff_to_value_for_bool.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:diff_to_value_for_bool.smt2}))))
(rule (alias runtest) (action (diff oracle diff_to_value_for_bool.smt2.res)))
-(rule (action (with-stdout-to diff_value_substupfalse.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:diff_value_substupfalse.smt2}))))
+(rule (action (with-stdout-to diff_value_substupfalse.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:diff_value_substupfalse.smt2}))))
(rule (alias runtest) (action (diff oracle diff_value_substupfalse.smt2.res)))
-(rule (action (with-stdout-to distinct.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:distinct.smt2}))))
+(rule (action (with-stdout-to distinct.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:distinct.smt2}))))
(rule (alias runtest) (action (diff oracle distinct.smt2.res)))
-(rule (action (with-stdout-to eq_diamond2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:eq_diamond2.smt2}))))
+(rule (action (with-stdout-to eq_diamond2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:eq_diamond2.smt2}))))
(rule (alias runtest) (action (diff oracle eq_diamond2.smt2.res)))
-(rule (action (with-stdout-to equality_norm_set.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:equality_norm_set.smt2}))))
+(rule (action (with-stdout-to equality_norm_set.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:equality_norm_set.smt2}))))
(rule (alias runtest) (action (diff oracle equality_norm_set.smt2.res)))
-(rule (action (with-stdout-to fundef.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:fundef.smt2}))))
+(rule (action (with-stdout-to fundef.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:fundef.smt2}))))
(rule (alias runtest) (action (diff oracle fundef.smt2.res)))
-(rule (action (with-stdout-to get_repr_at__instead_of__equal_CRepr.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:get_repr_at__instead_of__equal_CRepr.smt2}))))
+(rule (action (with-stdout-to get_repr_at__instead_of__equal_CRepr.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:get_repr_at__instead_of__equal_CRepr.smt2}))))
(rule (alias runtest) (action (diff oracle get_repr_at__instead_of__equal_CRepr.smt2.res)))
-(rule (action (with-stdout-to many_distinct.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:many_distinct.smt2}))))
+(rule (action (with-stdout-to many_distinct.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:many_distinct.smt2}))))
(rule (alias runtest) (action (diff oracle many_distinct.smt2.res)))
-(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:polyeq_genequality.smt2}))))
+(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:polyeq_genequality.smt2}))))
(rule (alias runtest) (action (diff oracle polyeq_genequality.smt2.res)))
-(rule (action (with-stdout-to polyeq_genequality_deltaed.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:polyeq_genequality_deltaed.smt2}))))
+(rule (action (with-stdout-to polyeq_genequality_deltaed.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:polyeq_genequality_deltaed.smt2}))))
(rule (alias runtest) (action (diff oracle polyeq_genequality_deltaed.smt2.res)))
-(rule (action (with-stdout-to xor.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:xor.smt2}))))
+(rule (action (with-stdout-to xor.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:xor.smt2}))))
(rule (alias runtest) (action (diff oracle xor.smt2.res)))
--
GitLab