Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

smt_compliant setting makes script unknown with a bizarre reason #7362

Closed
LeventErkok opened this issue Aug 30, 2024 · 0 comments
Closed

smt_compliant setting makes script unknown with a bizarre reason #7362

LeventErkok opened this issue Aug 30, 2024 · 0 comments

Comments

@LeventErkok
Copy link

LeventErkok commented Aug 30, 2024

The attached script results in unknown. It prints:

unknown
(:reason-unknown "Sort mismatch at argument #2 for function (declare-fun = (Real Real) Bool) supplied sort is Int")

The unknown reason is truly confusing. There are no Real's in the benchmark, it's all about integers.

Surprisingly, if I comment out the very first line:

(set-option :smtlib2_compliant true)

then I get sat as the answer.

buggy.txt

@LeventErkok LeventErkok changed the title Bizarre "unknown" reason with smt_compliant setting smt_compliant setting makes script unknown with a bizarre result Aug 30, 2024
@LeventErkok LeventErkok changed the title smt_compliant setting makes script unknown with a bizarre result smt_compliant setting makes script unknown with a bizarre reason Aug 30, 2024
NikolajBjorner added a commit that referenced this issue Aug 30, 2024
Signed-off-by: Nikolaj Bjorner <[email protected]>
NikolajBjorner added a commit that referenced this issue Aug 30, 2024
Signed-off-by: Nikolaj Bjorner <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants