3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00

fix string theory setup so that string-integer integration actually works

This commit is contained in:
Murphy Berzish 2016-06-07 17:38:57 -04:00
parent e0df5bc2ed
commit 62aeff90c5

View file

@ -706,7 +706,7 @@ namespace smt {
}
void setup::setup_QF_S() {
setup_QF_LRA();
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
m_context.register_plugin(alloc(smt::theory_str, m_manager));
}