QF_SNRA: Incompleteness with implicit real to int conversion

[maurobringolf]

Commit: 2c35a4fd262a7aa1cc3b953265d327de4eae9f8e

$ cvc5 -q --strings-exp unknown.smt2
unknown
$ cvc5 --force-logic=SNRA unknown.smt2
unknown
$ cvc5 --force-logic=QF_SNRA unknown.smt2
unknown
$ z3 unknown.smt2
sat
$ cat unknown.smt2
(declare-fun s () Real)
(declare-fun k () Real)
(assert (or (> (* s s) (str.to_int "3")) (= 0.0 k)))
(check-sat)
$ cvc5 -q --strings-exp known.smt2
sat
$ cat known.smt2
(declare-fun s () Real)
(declare-fun k () Real)
(assert (and (> (* s s) (str.to_int "3")) (= 0.0 k)))
(check-sat)

To me this seems unexpected, as two simple independent subformulas can be solved as a conjunction but not as a disjunction.

[ajreynol]

(str.to_int "3") can be replaced by 3 without impacting the behavior.

This is a case where non-linear real arithmetic cannot solve due to using a logic where nl-cad is disabled by default.