Nondeterministic error '(error "tactic failed: canceled")' with check-sat-using par-or

[mschwerhoff]

Running a self-compiled x32 build of Z3 revision 294dcf7 on Windows 10 x64 on this SMT-LIB file, I non-deterministically get (error "tactic failed: canceled") errors. The error isn't easy to reproduce, though: on my machine, it takes about 3000 Z3 runs with varying random seeds to observe it.

A few observations I've made:

• Removing (set-option :timeout 10) before check-sat-using seems to make the problem disappear
• The rlimit-delta is always 17, for both successful and erroneous runs
• Whenever I removed larger parts of the file, I could no longer reproduce the problem
• Using a debug build of the same Z3 revision, I also could no longer reproduce the problem, even with > 10K executions

Please let me know if there is anything I can do to help.

Thank you,
Malte

[mschwerhoff]

Thank you for fixing the issue so quickly!