Open chyanju opened 11 months ago
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!