search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.41k stars 1.47k forks source link

"mbp to_real" when using spacer with global guidance #7285

Closed mmsbrggr closed 1 month ago

mmsbrggr commented 4 months ago

I modeled a version of the "temperature control system" using Horn clauses and trying to prove deadlock-freedom. For certain initial values (max/min temperature, etc.) I noticed that Spacer gets stuck in generating similar invariants that just differ in one integer. Therefore, I enabled the global guidance option "spacer.global". However, after enabling the option Z3 terminates with "unknown" and reason "mbp to_real".

There are only integers (and enums) in the encoding. Moreover, even enabling "rewriter.elim_to_real" didn't solve the problem.

Here is the exported smt-lib encoding: temperature.smt2.txt

hgvk94 commented 4 months ago

I have solved this problem in my local branch: https://github.com/hgvk94/z3/commit/aad4cac4b83378a45230d550c2fead0561c3aa94 I will merge it soon. However, even after the fix, global guidance doesn't solve this instance. It identifies the common pattern but doesn't know how to generalize it.

mmsbrggr commented 4 months ago

Thank you! I will test it with your branch.