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

fix #2778

Browse source
This commit is contained in:
Nikolaj Bjorner 2019-12-03 12:53:06 +01:00
parent 9af4cc0fd6
commit b35ec49b40
1 changed files with 7 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/theory_diff_logic_def.h
View file

@ -192,10 +192,13 @@ bool theory_diff_logic<Ext>::internalize_atom(app * n, bool gate_ctx) {
found_non_diff_logic_expr(n); found_non_diff_logic_expr(n);
return false; return false;
} }
SASSERT(m_signs.size() == m_terms.size());
if (m_terms.size() == 2 && m_signs[0] != m_signs[1]) { if (m_terms.size() == 2 && m_signs[0] != m_signs[1]) {
target = mk_var(m_terms[0].get()); app* a = m_terms.get(0), *b = m_terms.get(1);
source = mk_var(m_terms[1].get()); bool sign0 = m_signs[0];
if (!m_signs[0]) { target = mk_var(a);
source = mk_var(b);
if (!sign0) {
std::swap(target, source); std::swap(target, source);
} }
} }
@ -384,7 +387,7 @@ void theory_diff_logic<Ext>::del_atoms(unsigned old_size) {
template<typename Ext> template<typename Ext>
bool theory_diff_logic<Ext>::decompose_linear(app_ref_vector& terms, svector<bool>& signs) { bool theory_diff_logic<Ext>::decompose_linear(app_ref_vector& terms, svector<bool>& signs) {
for (unsigned i = 0; i < terms.size(); ++i) { for (unsigned i = 0; i < terms.size(); ++i) {
app* n = terms[i].get(); app* n = terms.get(i);
bool sign; bool sign;
if (m_util.is_add(n)) { if (m_util.is_add(n)) {
expr* arg = n->get_arg(0); expr* arg = n->get_arg(0);