From 50f5cafb5048e788ce6b314db68ed2bd838b6972 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 1 Aug 2021 05:09:58 -0700
Subject: [PATCH] fix #5446

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/arith/fm_tactic.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp
index 44b771d53..f87261dcf 100644
--- a/src/tactic/arith/fm_tactic.cpp
+++ b/src/tactic/arith/fm_tactic.cpp
@@ -162,7 +162,7 @@ class fm_tactic : public tactic {
         fm_model_converter(ast_manager & _m):m(_m) {}
 
         ~fm_model_converter() override {
-            m.dec_array_ref(m_xs.size(), m_xs.data());
+            m.dec_array_ref(m_xs.size(), m_xs.data());           
             vector<clauses>::iterator it  = m_clauses.begin();
             vector<clauses>::iterator end = m_clauses.end();
             for (; it != end; ++it)
@@ -1598,7 +1598,7 @@ class fm_tactic : public tactic {
                 report_tactic_progress(":fm-cost", m_counter);
                 if (!m_inconsistent) {
                     copy_remaining();
-                    m_new_goal->add(concat(g->mc(), m_mc.get()));
+                    m_new_goal->add(m_mc.get());
                 }
             }
             reset_constraints();