From 31a5bd7fd7dc401f0af99261900f0b706c18aba4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 9 May 2021 20:33:39 -0700 Subject: [PATCH] regression from July 4 2020 tweeted by Dr. RJ and crowd profiled - let's submit this somwhere? Signed-off-by: Nikolaj Bjorner --- src/ast/expr_substitution.h | 2 +- src/sat/smt/sat_dual_solver.cpp | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ast/expr_substitution.h b/src/ast/expr_substitution.h index ae02e371e..bbd1c0e8e 100644 --- a/src/ast/expr_substitution.h +++ b/src/ast/expr_substitution.h @@ -51,7 +51,7 @@ public: void reset(); void cleanup(); - obj_map const sub() const { return m_subst; } + obj_map const & sub() const { return m_subst; } std::ostream& display(std::ostream& out); }; diff --git a/src/sat/smt/sat_dual_solver.cpp b/src/sat/smt/sat_dual_solver.cpp index 22af58d59..7a48f8809 100644 --- a/src/sat/smt/sat_dual_solver.cpp +++ b/src/sat/smt/sat_dual_solver.cpp @@ -147,6 +147,7 @@ namespace sat { if (m_solver.value(r) == l_true) lits.push_back(r); out << "roots: " << lits << "\n"; + m_solver.display(out); return out; }