Test-api example for infer-loop attribute can be compiled even if infer-loop is disabled

parent fe790130
......@@ -690,7 +690,8 @@ The OCaml code that builds such a module is shown below.
:end-before: END{code1}
The debugging flags mentioned in :numref:`sec.runwithinferloop` can be
enabled using the API as follows:
enabled using the API as follows (the line(s) corresponding to the
desired flag(s) should be uncommented).
.. literalinclude:: ../examples/use_api/mlw_tree1.ml
:language: ocaml
......
......@@ -144,7 +144,9 @@ let mod_M1 =
(* END{code1} *)
(*BEGIN{flags}*)
let () = Debug.set_flag Infer_loop.print_inferred_invs
(* let () = Debug.set_flag Infer_cfg.infer_print_ai_result *)
(* let () = Debug.set_flag Infer_cfg.infer_print_cfg *)
(* let () = Debug.set_flag Infer_loop.print_inferred_invs *)
(*END{flags}*)
let mlw_file = Modules [ mod_M1 ]
......
......@@ -10,9 +10,6 @@ module M1
variant { Int.(-) 100 (Refint.(!) x) } Refint.incr x
done
end
### Debug: inferred invariants ###
forall w1:int. contents x <= 100
###
Tasks are:
Task 1: theory Task
type int
......@@ -232,15 +229,12 @@ Task 1: theory Task
goal f'vc :
forall x:int.
x <= 100 ->
x <= 100 /\
(forall x1:int.
x1 <= 100 ->
(if x1 < 100
then forall x2:int.
x2 = (x1 + 1) ->
(0 <= (100 - x1) /\ (100 - x2) < (100 - x1)) /\
x2 <= 100
else x1 = 100))
if x1 < 100
then forall x2:int.
x2 = (x1 + 1) ->
0 <= (100 - x1) /\ (100 - x2) < (100 - x1)
else x1 = 100)
end
On task 1, alt-ergo answers Valid (0.0xs, 8 steps)
On task 1, alt-ergo answers Unknown () (0.0xs)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment