search

Z3Prover / z3

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

Wrong solution of quantitative formula #7277

Closed Heaven2024 closed 2 months ago

Heaven2024 commented 3 months ago

Hi！ for this case： test.txt

cvc5 test.smt2 
sat

but z3 return unsat:

z3 test.smt2
unsat
Heaven2024 commented 3 months ago

same situation as: test2.txt These are benchmarks in practical applications

levnach commented 2 months ago

Actually, cvc5 gives unsat on both files. This is the version of cvc5 I checked with.

cvc5 --version "This is cvc5 version 1.1.2 [git tag 1.1.2 branch HEAD] compiled with GCC version 10-posix 20220113 on Mar 1 2024 17:23:36

Can you try to minimize and simplify the example?

Heaven2024 commented 2 months ago

Actually, cvc5 gives unsat on both files. This is the version of cvc5 I checked with.

cvc5 --version "This is cvc5 version 1.1.2 [git tag 1.1.2 branch HEAD] compiled with GCC version 10-posix 20220113 on Mar 1 2024 17:23:36

Can you try to minimize and simplify the example?

Thank you. The version I am using for cvc5 is 1.1.3. Maybe there are some errors in this version.