diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp index 94521be30..c82057a1c 100644 --- a/libsmtutil/CHCSmtLib2Interface.cpp +++ b/libsmtutil/CHCSmtLib2Interface.cpp @@ -189,7 +189,7 @@ std::string CHCSmtLib2Interface::querySolver(std::string const& _input) if (m_enabledSolvers.eld) return "eld"; if (m_enabledSolvers.z3) - return "z3 rlimit=1000000"; + return "z3 rlimit=1000000 fp.spacer.q3.use_qgen=true fp.spacer.mbqi=false fp.spacer.ground_pobs=false"; return ""; }(); auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + " " + solverBinary, _input);