mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-26 07:43:41 +00:00
Code Activity

fix

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-18 14:14:46 -08:00
parent 98bfbc2d62
commit 13e335f062
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/grobner/pdd_grobner.cpp
View file

@ -171,6 +171,7 @@ namespace dd {
m_stats.m_superposed++; m_stats.m_superposed++;
if (r.is_zero()) return; if (r.is_zero()) return;
equation* eq = alloc(equation, r, m_dep_manager.mk_join(eq1.dep(), eq2.dep()), m_equations.size()); equation* eq = alloc(equation, r, m_dep_manager.mk_join(eq1.dep(), eq2.dep()), m_equations.size());
m_equations.push_back(eq);
update_stats_max_degree_and_size(*eq); update_stats_max_degree_and_size(*eq);
check_conflict(*eq); check_conflict(*eq);
m_to_simplify.insert(eq); m_to_simplify.insert(eq);