From 3dad24ace0925c985bfca0d44ee1c991b7c93368 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 10 Mar 2020 15:11:24 -0700
Subject: [PATCH] fix #3225

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/nlsat/nlsat_solver.cpp | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index d6d035454..6c8affefb 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -2689,8 +2689,6 @@ namespace nlsat {
             u_map<literal> b2l;
             scoped_literal_vector lits(m_solver);
             svector<bool> even;
-            polynomial::manager::scoped_numeral cnst(m_pm.m());
-            m_pm.m().set(cnst, 1);
             unsigned num_atoms = m_atoms.size();
             for (unsigned j = 0; j < num_atoms; ++j) {
                 atom* a = m_atoms[j];