mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 17:08:45 +00:00
Code Activity

count gcd conflicts

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-04-25 16:31:56 -07:00
parent ace6e8eea1
commit 59bc070268
2 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_arith_core.h
View file

@ -1735,7 +1735,6 @@ namespace smt {
m_util(m), m_util(m),
m_arith_eq_solver(m), m_arith_eq_solver(m),
m_arith_eq_adapter(*this, m_util), m_arith_eq_adapter(*this, m_util),
m_asserted_qhead(0),
m_row_vars_top(0), m_row_vars_top(0),
m_to_patch(1024), m_to_patch(1024),
m_blands_rule(false), m_blands_rule(false),

2
src/smt/theory_arith_int.h
View file

@ -754,6 +754,7 @@ namespace smt {
if (!(consts / gcds).is_int()) { if (!(consts / gcds).is_int()) {
TRACE("gcd_test", tout << "row failed the GCD test:\n"; display_row_info(tout, r);); TRACE("gcd_test", tout << "row failed the GCD test:\n"; display_row_info(tout, r););
antecedents ante(*this); antecedents ante(*this);
m_stats.m_gcd_conflicts++;
collect_fixed_var_justifications(r, ante); collect_fixed_var_justifications(r, ante);
context & ctx = get_context(); context & ctx = get_context();
ctx.set_conflict( ctx.set_conflict(
@ -833,6 +834,7 @@ namespace smt {
numeral u1 = floor(u/gcds); numeral u1 = floor(u/gcds);
if (u1 < l1) { if (u1 < l1) {
m_stats.m_gcd_conflicts++;
TRACE("gcd_test", tout << "row failed the extended GCD test:\n"; display_row_info(tout, r);); TRACE("gcd_test", tout << "row failed the extended GCD test:\n"; display_row_info(tout, r););
collect_fixed_var_justifications(r, ante); collect_fixed_var_justifications(r, ante);
context & ctx = get_context(); context & ctx = get_context();