From da27edfd9e12f71ebb587962b64081c3dd62ce62 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 9 Mar 2020 07:20:13 +0100
Subject: [PATCH] fix #3215

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

diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 1b3dcd260..d8d84218c 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -800,6 +800,7 @@ namespace nlsat {
             imp& checker = *(solver2.m_imp);
             checker.m_check_lemmas = false;
             checker.m_log_lemmas = false;
+            checker.m_inline_vars = false;
 
             // need to translate Boolean variables and literals
             svector<bool_var> tr;