From 2d01c64d2cf6430e186ef882d3e74b3d37cdf025 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 2 Apr 2020 12:30:25 -0700
Subject: [PATCH] fix #3682

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

diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp
index 7d22ef682..bcfff4043 100644
--- a/src/tactic/smtlogics/qfufbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfufbv_tactic.cpp
@@ -70,8 +70,15 @@ public:
         flas.reset();
         // report result
         goal_ref resg(alloc(goal, *g, true));
-        if (o == l_false) resg->assert_expr(m.mk_false());
-        if (o != l_undef) result.push_back(resg.get());
+        if (o == l_false) 
+            resg->assert_expr(m.mk_false());
+        if (o == l_undef) {
+            g->inc_depth();
+            result.push_back(g.get());
+        }
+        else {
+            result.push_back(resg.get());
+        }
         // report model
         if (g->models_enabled() && o == l_true) {
             model_ref abstr_model = imp.get_model();