Petiot 2018 experiments not reproducible with Z3
Currently the reproducible generation of counterexamples with Z3 using option --stepslimit
of why3 prove
doesn't seem to be possible: the counterexamples are missing, or unrelated to the counterexample generated without steps limit, even when using the reported steps as limit.
A step limit is currently handed over to Z3 by option memory_max_alloc_count
, resulting in the mentioned problem. Is this actually related to the steps reported by why3 prove
?
Using the newer Z3 option rlimit
doesn't help either because it seems to give a limit on the overall call to Z3, whereas we would need a limit on the individual queries (get-model)
(as CVC4's --rlimit-per
).