Commit 382abb786 routed theory::mk_literal through the new
context::non_ground_internalize helper. For a top-level quantifier
literal (e.g. the universally-quantified emptiness condition produced
by the sequence/regex solver), that helper takes the non-ground proxy
path — it allocates a fresh proxy constant, asserts proxy = quantifier
and internalizes assertions — instead of internalizing the quantifier
directly. This engages quantifier instantiation on a goal the seq
theory previously discharged instantly as incomplete, turning a fast
'unknown (incomplete (theory seq))' answer into a -T: timeout.
Restore the previous behavior for quantifier expressions by
internalizing them directly, while keeping non_ground_internalize for
all other (non-quantifier) expressions.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
9b8bfe6a26