z3 hangs on query involving maps and bitvectors #7484
Description
Hi z3 team -- my student @vrindisbacher came across the following two SMTLIB queries that seem to finish instantaneously with cvc5 but seem to make z3 hang indefinitely. I will ask John Regehr's help with using c-reduce to minimize the tests -- but maybe you have some idea?
There are two files.
The first test z3-slow-1.smt2.txt should work just by pure equality/congruence.
There is a lot of junk in it but we're just checking a VC of the form. (a = b) => (a = b)
(assert (= a b))
(assert (not (= a b)))
(check-sat)
except that that the a and b are blown out into gigantic terms involving map-set
and bitvector operations, with some additional booleans recording the equality...
The second is not so trivial, but both seem to finish swiftly with CVC5.
Any ideas on what might be happening?