Unknown sort 'Int' when using `QF_NRA theory

[chyanju]

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!