Closed
Description
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.
Metadata
Metadata
Assignees
Labels
No labels