From 525738612048441a6c92f5497c8f29edde383707 Mon Sep 17 00:00:00 2001 From: Stevendeo Date: Fri, 24 Nov 2023 08:42:25 +0100 Subject: [PATCH] Cleaner handling of step limit (#936) * Treating step limit as an unknown reason and not a fatal error * Update env when step limit is reached * Also update env in fun_sat * Rebase artifact * Update frontend to handle query when unknown is already decided * Steps as a dolmen option * Adding missing file * Poetry * Poetry * Rebase artifacts --- src/bin/common/parse_command.ml | 1 + src/bin/common/solving_loop.ml | 16 ++++ src/bin/js/worker_js.ml | 9 +-- src/lib/frontend/d_state_option.ml | 6 ++ src/lib/frontend/d_state_option.mli | 6 ++ src/lib/frontend/frontend.ml | 81 ++++++++++++------- src/lib/frontend/frontend.mli | 2 +- src/lib/reasoners/fun_sat.ml | 8 +- src/lib/reasoners/sat_solver_sig.ml | 2 + src/lib/reasoners/sat_solver_sig.mli | 1 + src/lib/reasoners/satml_frontend.ml | 32 +++++--- src/lib/structures/errors.ml | 3 - src/lib/structures/errors.mli | 1 - src/lib/util/steps.ml | 26 ++++-- src/lib/util/steps.mli | 13 ++- src/lib/util/util.ml | 1 + src/lib/util/util.mli | 1 + tests/dune.inc | 21 +++++ .../testfile-steps-bound.dolmen.expected | 5 ++ tests/smtlib/testfile-steps-bound.dolmen.smt2 | 26 ++++++ 20 files changed, 201 insertions(+), 60 deletions(-) create mode 100644 tests/smtlib/testfile-steps-bound.dolmen.expected create mode 100644 tests/smtlib/testfile-steps-bound.dolmen.smt2 diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index dfe1b3e9a..f004be9ca 100644 --- a/src/bin/common/parse_command.ml +++ b/src/bin/common/parse_command.ml @@ -362,6 +362,7 @@ let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation set_fm_cross_limit fm_cross_limit; set_timelimit_interpretation timelimit_interpretation; set_steps_bound steps_bound; + Steps.set_steps_bound steps_bound; set_timelimit timelimit; set_timelimit_per_goal timelimit_per_goal; `Ok() diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index ea8f4b753..9531495cb 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -316,6 +316,15 @@ let main () = State.create_key ~pipe:"" "named_terms" in + let set_steps_bound i st = + try DO.Steps.set i st with + Invalid_argument _ -> (* Raised by Steps.set_steps_bound *) + fatal_error + "Error while setting steps bound to %i: current step = %i." + i + (Steps.get_steps ()) + in + let debug_parsed_pipe st c = if State.get State.debug st then Format.eprintf "[logic][parsed][%a] @[%a@]@." @@ -477,6 +486,7 @@ let main () = sat; st | Tableaux | Tableaux_CDCL | CDCL | CDCL_Tableaux -> + O.set_sat_solver sat; (* `make_sat` returns the sat solver corresponding to the new sat_solver option. *) DO.SatSolver.set sat st @@ -608,6 +618,12 @@ let main () = | Some b -> set_optimize b st end + | ":steps-bound", Symbol { name = Simple level; _ } -> + begin + match int_of_string_opt level with + | None -> print_wrn_opt ~name st_loc "integer" value; st + | Some i -> set_steps_bound i st + end | _ -> unsupported_opt name; st in diff --git a/src/bin/js/worker_js.ml b/src/bin/js/worker_js.ml index 7b6a1c46c..c2ac73feb 100644 --- a/src/bin/js/worker_js.ml +++ b/src/bin/js/worker_js.ml @@ -179,13 +179,8 @@ let main worker_id content = raise Exit | Errors.Error e -> begin match e with - | Errors.Run_error r -> begin - match r with - | Steps_limit _ -> - returned_status := - Worker_interface.LimitReached "Steps limit" - | _ -> returned_status := Worker_interface.Error "Run error" - end + | Errors.Run_error _ -> + returned_status := Worker_interface.Error "Run error" | _ -> returned_status := Worker_interface.Error "Error" end; Printer.print_err "%a" Errors.report e; diff --git a/src/lib/frontend/d_state_option.ml b/src/lib/frontend/d_state_option.ml index 6a6181afc..5fdf04332 100644 --- a/src/lib/frontend/d_state_option.ml +++ b/src/lib/frontend/d_state_option.ml @@ -99,6 +99,12 @@ let msatsolver = module SatSolver = (val msatsolver) +let msteps = + let on_update _ sat st = Steps.set_steps_bound sat; st in + (create_opt ~on_update "steps_bound" O.get_steps_bound) + +module Steps = (val msteps) + (* Some options can be initialized to gain some performance. *) let options_requiring_initialization = [ (module SatSolverModule : S); diff --git a/src/lib/frontend/d_state_option.mli b/src/lib/frontend/d_state_option.mli index f4989606f..70472f77a 100644 --- a/src/lib/frontend/d_state_option.mli +++ b/src/lib/frontend/d_state_option.mli @@ -64,5 +64,11 @@ module SatSolver : S with type t = Util.sat_solver on SatSolver: when SatSolver is updated, this one also is. *) module SatSolverModule : Accessor with type t = (module Sat_solver_sig.S) +(** Option for setting the max number of steps. Interfaces with the toplevel + Steps module. + The [set] function may raise Invalid_arg from the Steps.set_steps_bound call + if the new option value is lower than the current number of steps. *) +module Steps : S with type t = int + (** Initializes the state with options that requires some preprocessing. *) val init : D_loop.Typer.state -> D_loop.Typer.state diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index ecf5ec02e..3883df88e 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -142,7 +142,7 @@ module type S = sig mutable expl : Explanation.t } - type 'a process = ?loc : Loc.t -> env -> 'a -> unit + type 'a process = ?loc : Loc.t -> 'a -> env -> unit val init_env : ?sat_env:sat_env -> used_context -> env @@ -226,7 +226,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct mutable expl : Explanation.t } - type 'a process = ?loc : Loc.t -> env -> 'a -> unit + type 'a process = ?loc : Loc.t -> 'a -> env -> unit let init_env ?(sat_env=SAT.empty ()) used_context = { @@ -300,13 +300,14 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct if Options.get_unsat_core () then Ex.singleton (Ex.RootDep {name;f;loc}) else Ex.empty - let internal_push ?(loc = Loc.dummy) (env : env) (n : int) : unit = + let internal_push ?(loc = Loc.dummy) (n : int) (env : env) : unit = ignore loc; Util.loop ~f:(fun _ res () -> Stack.push res env.consistent_dep_stack) ~max:n ~elt:(env.res, env.expl) ~init:(); + Steps.apply_without_step_limit (fun () -> SAT.push env.sat_env n); SAT.push env.sat_env n - let internal_pop ?(loc = Loc.dummy) (env : env) (n : int) : unit = + let internal_pop ?(loc = Loc.dummy) (n : int) (env : env) : unit = ignore loc; let res, expl = Util.loop ~f:(fun _n () _env -> Stack.pop env.consistent_dep_stack) @@ -318,8 +319,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct let internal_assume ?(loc = Loc.dummy) - (env : env) - ((name, f, mf) : string * E.t * bool) = + ((name, f, mf) : string * E.t * bool) + (env : env) = let is_hyp = try (Char.equal '@' name.[0]) with _ -> false in if is_hyp || not (unused_context name env.used_context) then let expl = @@ -349,13 +350,13 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct | `Unsat -> env.expl <- expl - let internal_pred_def ?(loc = Loc.dummy) env (name, f) = + let internal_pred_def ?(loc = Loc.dummy) (name, f) env = if not (unused_context name env.used_context) then let expl = mk_root_dep name f loc in SAT.pred_def env.sat_env f name expl loc; env.expl <- expl - let internal_query ?(loc = Loc.dummy) env (n, f, sort) = + let internal_query ?(loc = Loc.dummy) (n, f, sort) env = ignore loc; let expl = match env.res with @@ -385,8 +386,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct let internal_th_assume ?(loc = Loc.dummy) - env - ({ Expr.ax_name; Expr.ax_form ; _ } as th_elt) = + ({ Expr.ax_name; Expr.ax_form ; _ } as th_elt) + env = if not (unused_context ax_name env.used_context) then match env.res with | `Sat | `Unknown -> @@ -395,8 +396,13 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct env.expl <- expl | `Unsat -> () - let handle_sat_exn f ?loc env x = - try f ?loc env x with + let check_step_limit f env = + match SAT.get_unknown_reason env.sat_env with + | Some (Step_limit _) -> () + | _ -> f env + + let handle_sat_exn f ?loc x env = + try f ?loc x env with | SAT.Sat -> env.res <- `Sat | SAT.Unsat expl -> env.res <- `Unsat; @@ -405,35 +411,54 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct env.res <- `Unknown (* The SAT.Timeout exception is not catched. *) - let push = handle_sat_exn internal_push + (* Wraps the function f to check if the step limit is reached (in which case, + don't do anything), and then calls the function & catches the + exceptions. *) + let wrap_f f ?loc x env = + check_step_limit (handle_sat_exn f ?loc x) env + + let push = wrap_f internal_push - let pop = handle_sat_exn internal_pop + let pop = wrap_f internal_pop - let assume = handle_sat_exn internal_assume + let assume = wrap_f internal_assume - let pred_def = handle_sat_exn internal_pred_def + let pred_def = wrap_f internal_pred_def - let query = handle_sat_exn internal_query + let query = wrap_f internal_query - let th_assume = handle_sat_exn internal_th_assume + let th_assume = wrap_f internal_th_assume let process_decl ?(hook_on_status=(fun _ -> ignore)) env d = try match d.st_decl with - | Push n -> internal_push ~loc:d.st_loc env n - | Pop n -> internal_pop ~loc:d.st_loc env n - | Assume (n, f, mf) -> internal_assume ~loc:d.st_loc env (n, f, mf) - | PredDef (f, name) -> internal_pred_def ~loc:d.st_loc env (name, f) + | Push n -> check_step_limit (internal_push ~loc:d.st_loc n) env + | Pop n -> check_step_limit (internal_pop ~loc:d.st_loc n) env + | Assume (n, f, mf) -> + check_step_limit (internal_assume ~loc:d.st_loc (n, f, mf)) env + | PredDef (f, name) -> + check_step_limit (internal_pred_def ~loc:d.st_loc (name, f)) env | RwtDef _ -> assert false | Query (n, f, sort) -> begin - internal_query ~loc:d.st_loc env (n, f, sort); - match env.res with - | `Unsat -> - hook_on_status (Unsat (d, env.expl)) (Steps.get_steps ()) - | _ -> assert false + (* If we have reached an unknown state, we can return it right + away. *) + match SAT.get_unknown_reason env.sat_env with + | Some (Step_limit _) -> raise SAT.I_dont_know + | Some _ -> + (* For now, only the step limit is an unknown step reachable + here. We could raise SAT.I_dont_know as in the previous case, + but we have choosen a defensive strategy. *) + assert false + | None -> + internal_query ~loc:d.st_loc (n, f, sort) env; + match env.res with + | `Unsat -> + hook_on_status (Unsat (d, env.expl)) (Steps.get_steps ()) + | _ -> assert false end - | ThAssume th_elt -> internal_th_assume ~loc:d.st_loc env th_elt + | ThAssume th_elt -> + check_step_limit (internal_th_assume ~loc:d.st_loc th_elt) env with | SAT.Sat -> (* This case should mainly occur when a query has a non-unsat result, diff --git a/src/lib/frontend/frontend.mli b/src/lib/frontend/frontend.mli index b79fa819a..507ac5f3a 100644 --- a/src/lib/frontend/frontend.mli +++ b/src/lib/frontend/frontend.mli @@ -68,7 +68,7 @@ module type S = sig They catch the [Sat], [Unsat] and [I_dont_know] exceptions to update the frontend environment, but not the [Timeout] exception which is raised to the user. *) - type 'a process = ?loc:Loc.t -> env -> 'a -> unit + type 'a process = ?loc:Loc.t -> 'a -> env -> unit val push : int process diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index b67c4965f..b71ec82a3 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -1630,7 +1630,8 @@ module Make (Th : Theory.S) = struct { acc.guards with current_guard = new_guard; guards = guards; - }}) + }} + ) ~max:to_push ~elt:() ~init:env @@ -1735,6 +1736,7 @@ module Make (Th : Theory.S) = struct assert (Ex.has_no_bj dep); dep | Util.Timeout -> model_gen_on_timeout env + | Util.Step_limit_reached n -> i_dont_know env (Step_limit n) let add_guard env gf = let current_guard = env.guards.current_guard in @@ -1753,6 +1755,10 @@ module Make (Th : Theory.S) = struct (* don't attempt to compute a model if timeout before calling unsat function *) i_dont_know env (Timeout Assume) + | Util.Step_limit_reached n -> + (* When reaching the step limit on an assume, we do not want to answer + 'unknown' right away. *) + {env with unknown_reason = Some (Step_limit n)} let pred_def env f name dep _loc = Debug.pred_def f; diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index 5c3559a09..37155faff 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/src/lib/reasoners/sat_solver_sig.ml @@ -40,11 +40,13 @@ type timeout_reason = type unknown_reason = | Incomplete | Memout + | Step_limit of int | Timeout of timeout_reason let pp_unknown_reason ppf = function | Incomplete -> Fmt.pf ppf "Incomplete" | Memout -> Fmt.pf ppf "Memout" + | Step_limit i -> Fmt.pf ppf "Step limit: %i" i | Timeout t -> Fmt.pf ppf "Timeout:%a" pp_timeout_reason t let pp_unknown_reason_opt ppf = function diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli index a8d7a0fdb..978752510 100644 --- a/src/lib/reasoners/sat_solver_sig.mli +++ b/src/lib/reasoners/sat_solver_sig.mli @@ -36,6 +36,7 @@ type timeout_reason = type unknown_reason = | Incomplete | Memout + | Step_limit of int | Timeout of timeout_reason val pp_unknown_reason: unknown_reason Fmt.t diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 071d5bcaa..9d5f39b94 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1260,11 +1260,17 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let push env to_push = Util.loop ~f:(fun _n () () -> - let expr_guard, atom_guard = create_guard env in - SAT.push env.satml atom_guard; - Stack.push expr_guard env.guards.stack_guard; - Steps.push_steps (); - env.guards.current_guard <- expr_guard + try + let expr_guard, atom_guard = create_guard env in + SAT.push env.satml atom_guard; + Stack.push expr_guard env.guards.stack_guard; + Steps.push_steps (); + env.guards.current_guard <- expr_guard + with + | Util.Step_limit_reached _ -> + (* This function should be called without step limit + (see Steps.apply_without_step_limit) *) + assert false ) ~max:to_push ~elt:() @@ -1331,12 +1337,16 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct assert (SAT.decision_level env.satml == 0); try ignore (assume_aux ~dec_lvl:0 env [add_guard env gf]) with | IUnsat (_env, dep) -> raise (Unsat dep) - (* Timeout -> I_dont_know conversions temporarily disabled - https://github.com/OCamlPro/alt-ergo/issues/946 *) - (* | Util.Timeout -> - (* don't attempt to compute a model if timeout before - calling unsat function *) - i_dont_know env (Timeout Assume) *) + (* Timeout -> I_dont_know conversions temporarily disabled + https://github.com/OCamlPro/alt-ergo/issues/946 *) + (* | Util.Timeout -> + (* don't attempt to compute a model if timeout before + calling unsat function *) + i_dont_know env (Timeout Assume) *) + | Util.Step_limit_reached n -> + (* When reaching the step limit on an assume, we do not want to + answer 'unknown' right away. *) + env.unknown_reason <- Some (Step_limit n) (* instrumentation of relevant exported functions for profiling *) let assume t ff dep = diff --git a/src/lib/structures/errors.ml b/src/lib/structures/errors.ml index bef21f1fc..c2f2d108f 100644 --- a/src/lib/structures/errors.ml +++ b/src/lib/structures/errors.ml @@ -81,7 +81,6 @@ type typing_error = type run_error = | Invalid_steps_count of int - | Steps_limit of int | Failed_check_unsat_core | Unsupported_feature of string | Dynlink_error of string @@ -229,8 +228,6 @@ let report_typing_error fmt = function let report_run_error fmt = function | Invalid_steps_count i -> fprintf fmt "%d is not a valid number of steps" i - | Steps_limit i -> - fprintf fmt "Steps limit reached: %d" i | Failed_check_unsat_core -> fprintf fmt "Checking produced unsat-core failed" | Unsupported_feature f -> diff --git a/src/lib/structures/errors.mli b/src/lib/structures/errors.mli index e66a5e4e3..59563364d 100644 --- a/src/lib/structures/errors.mli +++ b/src/lib/structures/errors.mli @@ -88,7 +88,6 @@ type typing_error = (** Errors that can be raised at solving*) type run_error = | Invalid_steps_count of int - | Steps_limit of int | Failed_check_unsat_core | Unsupported_feature of string | Dynlink_error of string diff --git a/src/lib/util/steps.ml b/src/lib/util/steps.ml index f859a7534..21c63d289 100644 --- a/src/lib/util/steps.ml +++ b/src/lib/util/steps.ml @@ -39,6 +39,8 @@ type incr_kind = | Th_assumed of int (* Increment the counter for each term assumed in the theories environment *) +let steps_bound = ref (Options.get_steps_bound ()) + let naive_steps = ref 0 let steps = ref 0 let mult_f = ref 0 @@ -104,17 +106,16 @@ let incr k = Errors.run_error (Invalid_steps_count n); naive_steps := !naive_steps + n; end; - let steps_bound = Options.get_steps_bound () in - if steps_bound <> -1 - && ((Stdlib.compare !steps ((steps_bound)) > 0) - || (Stdlib.compare !naive_steps ((steps_bound)) > 0)) then + if !steps_bound <> -1 + && ((Stdlib.compare !steps !steps_bound > 0) + || (Stdlib.compare !naive_steps !steps_bound > 0)) then begin let n = if !naive_steps > 0 then !naive_steps else if !steps > 0 then !steps - else steps_bound + else !steps_bound in - Errors.run_error (Steps_limit n) + raise (Util.Step_limit_reached n) end let reset_steps () = @@ -158,3 +159,16 @@ let get_steps () = let cs_steps_cpt = ref 0 let cs_steps () = !cs_steps_cpt let incr_cs_steps () = Stdlib.incr cs_steps_cpt + +let set_steps_bound i = + if get_steps () > i && i >= 0 then invalid_arg "Steps.set_steps_bound"; + steps_bound := i + +let get_steps_bound () = !steps_bound + +let apply_without_step_limit cont = + let bound = !steps_bound in + steps_bound := -1; + match cont () with + | res -> steps_bound := bound; res + | exception e -> steps_bound := bound; raise e diff --git a/src/lib/util/steps.mli b/src/lib/util/steps.mli index 33b139ea9..b8d4893f5 100644 --- a/src/lib/util/steps.mli +++ b/src/lib/util/steps.mli @@ -47,6 +47,12 @@ type incr_kind = theories environment *) (** Define the type of increment *) +(** Returns the max number of bounds *) +val get_steps_bound : unit -> int + +(** Sets the max number of bounds *) +val set_steps_bound : int -> unit + val incr : incr_kind -> unit (** Increment the number of steps depending of the incr_kind @raise Errors.Error.Invalid_steps_count if the number of steps is inbound @@ -54,7 +60,7 @@ val incr : incr_kind -> unit @raise Run_error {!Errors.Invalid_steps_count} if the number of steps sent to the theories is invalid. - {!Errors.Steps_limit} if the number of steps is reached *) + @raise {!Util.Step_limit_reached} if the number of steps is reached *) val reset_steps : unit -> unit (** Reset the global steps counter *) @@ -74,10 +80,13 @@ val cs_steps : unit -> int (** Increase the number of case-split steps *) val incr_cs_steps : unit -> unit +(** Disables the step limit during the execution of the continuation. *) +val apply_without_step_limit : (unit -> 'a) -> 'a + (** {2 Incrementality} *) val push_steps : unit -> unit (** Save all the steps value in an internal stack for each push command *) val pop_steps : unit -> unit -(** Pop the last steps value when a pop command is processed *) \ No newline at end of file +(** Pop the last steps value when a pop command is processed *) diff --git a/src/lib/util/util.ml b/src/lib/util/util.ml index fdbe3b2ba..2ac39acfa 100644 --- a/src/lib/util/util.ml +++ b/src/lib/util/util.ml @@ -29,6 +29,7 @@ (**************************************************************************) exception Timeout +exception Step_limit_reached of int exception Unsolvable exception Cmp of int diff --git a/src/lib/util/util.mli b/src/lib/util/util.mli index 9a6d6e115..7fa2b0976 100644 --- a/src/lib/util/util.mli +++ b/src/lib/util/util.mli @@ -29,6 +29,7 @@ (**************************************************************************) exception Timeout +exception Step_limit_reached of int exception Unsolvable exception Cmp of int diff --git a/tests/dune.inc b/tests/dune.inc index ef3858853..715dd86ae 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -204292,6 +204292,27 @@ ; Auto-generated part begin (subdir smtlib + (rule + (target testfile-steps-bound.dolmen_dolmen.output) + (deps (:input testfile-steps-bound.dolmen.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps testfile-steps-bound.dolmen_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-steps-bound.dolmen.expected testfile-steps-bound.dolmen_dolmen.output))) (rule (target testfile-reset_ci_cdcl_no_minimal_bj.output) (deps (:input testfile-reset.smt2)) diff --git a/tests/smtlib/testfile-steps-bound.dolmen.expected b/tests/smtlib/testfile-steps-bound.dolmen.expected new file mode 100644 index 000000000..512df716c --- /dev/null +++ b/tests/smtlib/testfile-steps-bound.dolmen.expected @@ -0,0 +1,5 @@ + +unknown +(:reason-unknown Step limit: 3) + +unsat diff --git a/tests/smtlib/testfile-steps-bound.dolmen.smt2 b/tests/smtlib/testfile-steps-bound.dolmen.smt2 new file mode 100644 index 000000000..ed9711b98 --- /dev/null +++ b/tests/smtlib/testfile-steps-bound.dolmen.smt2 @@ -0,0 +1,26 @@ +(set-logic ALL) + +(declare-const x Int) +(declare-const y Int) +(assert (= (* x x) 3)) + +(push 1) +; Setting this option here should fail because the previous assertion takes +; more than 2 steps. It does not because AE does not execute SMTLIB instruction +; imperatively; here, the option is actually set before the assertion is +; executed. +(set-option :steps-bound 2) +; Should answer 'unknown' +(check-sat) +(get-info :reason-unknown) +(pop 1) + +(reset) + +(set-logic ALL) +(declare-const x Int) +(declare-const y Int) +(set-option :steps-bound 100) +; Should answer 'unsat' +(assert (= (* x x) 3)) +(check-sat) \ No newline at end of file