From 7996472923e9985705f46ba838cc9ec8c88ba563 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 17 Mar 2020 10:37:50 -0700
Subject: [PATCH] fix ? #3370
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/theory_arith_int.h | 2 ++
src/smt/theory_diff_logic_def.h | 6 ++++--
src/tactic/core/solve_eqs_tactic.cpp | 9 ++++++++-
3 files changed, 14 insertions(+), 3 deletions(-)
diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index d46fa4350..5b0d70093 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -620,6 +620,8 @@ namespace smt {
expr_ref bound(get_manager());
if (pol.empty()) {
+ if (ante.lits().empty() && ante.eqs().empty())
+ return false;
SASSERT(k.is_pos());
// conflict 0 >= k where k is positive
set_conflict(ante, ante, "gomory-cut");
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index 31bdf30fd..c0c0c3a26 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -1237,8 +1237,10 @@ theory_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker, bool& has_shar
if (is_simplex_edge(v)) {
unsigned edge_id = simplex2edge(v);
literal lit = m_graph.get_explanation(edge_id);
- get_context().literal2expr(lit, tmp);
- core.push_back(tmp);
+ if (lit != null_literal) {
+ get_context().literal2expr(lit, tmp);
+ core.push_back(tmp);
+ }
}
}
compute_delta();
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index 6a84bedfc..455750ed9 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -49,6 +49,7 @@ class solve_eqs_tactic : public tactic {
expr_sparse_mark m_candidate_vars;
expr_sparse_mark m_candidate_set;
ptr_vector<expr> m_candidates;
+ expr_ref_vector m_marked_candidates;
ptr_vector<app> m_vars;
expr_sparse_mark m_nonzero;
ptr_vector<app> m_ordered_vars;
@@ -62,7 +63,8 @@ class solve_eqs_tactic : public tactic {
m_r_owner(r == nullptr || owner),
m_a_util(m),
m_num_steps(0),
- m_num_eliminated_vars(0) {
+ m_num_eliminated_vars(0),
+ m_marked_candidates(m) {
updt_params(p);
if (m_r == nullptr)
m_r = mk_default_expr_replacer(m);
@@ -421,6 +423,7 @@ class solve_eqs_tactic : public tactic {
m_candidates.push_back(f);
m_candidate_set.mark(f);
m_candidate_vars.mark(var);
+ m_marked_candidates.push_back(f);
if (m_produce_proofs) {
if (!pr)
pr = g.pr(idx);
@@ -440,6 +443,7 @@ class solve_eqs_tactic : public tactic {
m_candidate_vars.reset();
m_candidate_set.reset();
m_candidates.reset();
+ m_marked_candidates.reset();
m_vars.reset();
m_nonzero.reset();
app_ref var(m());
@@ -841,6 +845,8 @@ class solve_eqs_tactic : public tactic {
for (expr* v : m_vars) {
if (!m_candidate_vars.is_marked(v)) {
m_candidate_set.mark(m_candidates[idx], false);
+ m_marked_candidates.push_back(m_candidates[idx]);
+ m_marked_candidates.push_back(v);
}
++idx;
}
@@ -908,6 +914,7 @@ class solve_eqs_tactic : public tactic {
expr * f = g.form(idx);
TRACE("gaussian_leak", tout << "processing:\n" << mk_ismt2_pp(f, m()) << "\n";);
if (m_candidate_set.is_marked(f)) {
+ m_marked_candidates.push_back(f);
// f may be deleted after the following update.
// so, we must remove the mark before doing the update
m_candidate_set.mark(f, false);