Closed
Description
Hi,
For the following instance, cvc5 befcee5 debug build
$ cat small.smt2
(declare-fun r (Real) Int)
(assert (forall ((x Real) (i Int)) (= (> x (to_real i)) (= 0 (r x)))))
(check-sat)
$ cvc5 --enum-inst -q small.smt2
Fatal failure within void cvc5::internal::theory::quantifiers::RelevantDomain::compute() at /home/cvc5/src/theory/quantifiers/relevant_domain.cpp:187
Check failure
false
Relevant domain: bad type Real, expected Int
Aborted (core dumped)