mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-01 03:41:21 +00:00
Code Activity

#5331

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-07-19 15:58:10 -07:00
parent a64867942d
commit a8b433e6ac
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/solver/assertions/asserted_formulas.cpp
View file

@ -424,7 +424,8 @@ void asserted_formulas::apply_quasi_macros() {
TRACE("before_quasi_macros", display(tout);); TRACE("before_quasi_macros", display(tout););
vector<justified_expr> new_fmls; vector<justified_expr> new_fmls;
quasi_macros proc(m, m_macro_manager); quasi_macros proc(m, m_macro_manager);
while (proc(m_formulas.size() - m_qhead, while (m_qhead == 0 &&
proc(m_formulas.size() - m_qhead,
m_formulas.data() + m_qhead, m_formulas.data() + m_qhead,
new_fmls)) { new_fmls)) {
swap_asserted_formulas(new_fmls); swap_asserted_formulas(new_fmls);