mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
parent
decd69ac73
commit
f1193986c9
|
@ -770,6 +770,9 @@ namespace qe {
|
|||
while (!vars.empty());
|
||||
SASSERT(m_vars.back().empty());
|
||||
initialize_levels();
|
||||
if (has_uninterpreted(m, fml))
|
||||
throw tactic_exception("formula contains uninterpreted functions");
|
||||
|
||||
TRACE("qe", tout << fml << "\n";);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue