Hello!
I was trying to switch to a different theory when calling z3, but it seems that constants are preferably defined as "Int" at the backend under certain circumstances, which causes some theory (e.g., `QF_NRA) to fail. Here's an example:
(require rosette/solver/smt/z3)
(current-solver (z3 #:logic 'QF_NRA))
(output-smt #t)
(define-symbolic x real?)
(solve (assert (equal? -2.0 x)))
Executing the above code snippet results in:
read-solution: unrecognized solver output: (error line 12 column 18: Invalid function definition: unknown sort 'Int')
As I looked into the generated smt, the line that caused the error is:
(define-fun e0 () Int (- 2))
where "Int" is not supported in z3 when `QF_NRA is used.
Would there be any workaround or potential fix?
Thank you!
Hello!
I was trying to switch to a different theory when calling z3, but it seems that constants are preferably defined as "Int" at the backend under certain circumstances, which causes some theory (e.g., `QF_NRA) to fail. Here's an example:
Executing the above code snippet results in:
As I looked into the generated smt, the line that caused the error is:
where "Int" is not supported in z3 when `QF_NRA is used.
Would there be any workaround or potential fix?
Thank you!