search

Z3Prover / z3

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

Interpolation Problem Real-Int #217

Closed Heizmann closed 9 years ago

Heizmann commented 9 years ago

Executing Z3 ef7915858bca5e759ee0a34df2ae976e7e507bef with the command

z3 SMTLIB2_COMPLIANT\=true -t\:12000

on this SMT script, I obtain the following error message.

(error "line 74616 column 3676: Sort mismatch at argument #2 for function (declare-fun * (Real Real) Real) supplied sort is Int")

However, there is no Real in the script at all.

Heizmann commented 9 years ago

I just did. (Sorry for the dead link) Furthermore, I updated the arguments of my Z3 call. (Problem can be reproduced without smt.mbqi=false)

Heizmann commented 9 years ago

It seems that the problem only occurs if I use the argument SMTLIB2_COMPLIANT\=true.

NikolajBjorner commented 9 years ago

got it

NikolajBjorner commented 9 years ago

yes, it is the issue: the interpolants created mixed integer/real constraints. This is not expressible in SMT-LIB2's AUFLIRA theory. Is the compliant configuration required for your tool?

NikolajBjorner commented 9 years ago

fixed

Heizmann commented 9 years ago

Is the compliant configuration required for your tool? Once, we required it. I cannot remember the reason any more. In the last hours I run a few benchmarks without the compliant configuration and I have not noticed any problems.

NikolajBjorner commented 9 years ago

Right, but with the new fix you can use both compliant and non-compliant mode. Interpolation overwrites the portion that disables coercions in compliant mode.