From 051ede64e7102922601e53f24858978dd0a6d0e3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 4 Sep 2021 09:48:46 -0700
Subject: [PATCH] #5532

---
 src/sat/smt/sat_dual_solver.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/sat/smt/sat_dual_solver.cpp b/src/sat/smt/sat_dual_solver.cpp
index dcc90ddb0..599caf6e5 100644
--- a/src/sat/smt/sat_dual_solver.cpp
+++ b/src/sat/smt/sat_dual_solver.cpp
@@ -67,6 +67,7 @@ namespace sat {
         bool_var w = m_ext2var.get(v, null_bool_var);
         if (null_bool_var == w) {
             w = m_solver.mk_var();
+            m_solver.set_external(w);
             m_ext2var.setx(v, w, null_bool_var);
             m_var2ext.setx(w, v, null_bool_var);
             m_vars.push_back(v);
@@ -103,6 +104,7 @@ namespace sat {
             root = ext2lit(clause[0]);
         else {
             root = literal(m_solver.mk_var(), false);
+            m_solver.set_external(root.var());
             for (unsigned i = 0; i < sz; ++i)
                 m_solver.mk_clause(root, ~ext2lit(clause[i]), status::input());
         }