search

Z3Prover / z3

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

Incorrect solution regarding data type conversion #7272

Closed Heaven2024 closed 2 months ago

Heaven2024 commented 3 months ago

Hi! Z3 [version 4.13.1 - 64 bit] ubuntu:22.04

cat test.smt2
(declare-fun B () Real)
(assert (not (is_int (to_real (* 2 B)))))
(check-sat)
(exit)

cvc5 test.smt2  --check-models
sat

but for z3 :

z3 test.smt2
unsat
NikolajBjorner commented 2 months ago

to_real should really only be used on integer arguments. https://smt-lib.org/theories-Reals_Ints.shtml Z3 makes a choice to add a "to_int" conversion to arguments that are real when the argument should be int.

NikolajBjorner commented 2 months ago

C:\z3\build>z3 7272.smt2 /v:10 /tr:asserted_formulas /tr:rewriter /tr:th_rewriter_step smtlib2_compliant=true success (error "line 2 column 36: Sort mismatch at argument #2 for function (declare-fun * (Int Int) Int) supplied sort is Real")