mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

#5614 turn on / off options to get better performance.

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-11-11 17:54:46 -08:00
parent b28a8013fe
commit 63ac2ee0d1
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/lp_bound_propagator.h
View file

@ -146,7 +146,7 @@ class lp_bound_propagator {
unsigned v_j = v->column(); unsigned v_j = v->column();
unsigned j = null_lpvar; unsigned j = null_lpvar;
if (!lp().find_in_fixed_tables(val(v_j), is_int(v_j), j)) { if (!lp().find_in_fixed_tables(val(v_j), is_int(v_j), j)) {
// try_add_equation_with_internal_fixed_tables(row_index, v); try_add_equation_with_internal_fixed_tables(row_index, v);
return; return;
} }

2
src/smt/theory_lra.cpp
View file

@ -2084,7 +2084,7 @@ public:
while (m_asserted_qhead < m_asserted_atoms.size() && !ctx().inconsistent() && m.inc()) { while (m_asserted_qhead < m_asserted_atoms.size() && !ctx().inconsistent() && m.inc()) {
auto [bv, is_true] = m_asserted_atoms[m_asserted_qhead]; auto [bv, is_true] = m_asserted_atoms[m_asserted_qhead];
m_bv_to_propagate.push_back(bv); // m_bv_to_propagate.push_back(bv);
api_bound* b = nullptr; api_bound* b = nullptr;
TRACE("arith", tout << "propagate: " << literal(bv, !is_true) << "\n"; TRACE("arith", tout << "propagate: " << literal(bv, !is_true) << "\n";