From 005d35f9c931bf0c0bd6087285b2cb0af9d18944 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 21 Jul 2021 07:39:39 -0700
Subject: [PATCH] #5422
---
src/math/simplex/model_based_opt.cpp | 1 -
src/sat/smt/q_solver.cpp | 2 +-
2 files changed, 1 insertion(+), 2 deletions(-)
diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp
index 5bc0b1836..1acbb592b 100644
--- a/src/math/simplex/model_based_opt.cpp
+++ b/src/math/simplex/model_based_opt.cpp
@@ -1257,7 +1257,6 @@ namespace opt {
}
def result;
if (compute_def) {
- TRACE("opt1", tout << m_rows[row_id1] << "\n";);
result = def(m_rows[row_id1], x);
m_var2value[x] = eval(result);
TRACE("opt1", tout << "updated eval " << x << " := " << eval(x) << "\n";);
diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index 23276a3f1..5769340ee 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -51,7 +51,7 @@ namespace q {
for (expr* e : exp) {
sat::literal lit = ctx.internalize(e, l.sign(), false, false);
add_clause(~l, lit);
- ctx.add_aux(~l, lit);
+ ctx.add_root(~l, lit);
}
}
else {