From 3574a95e501c75bbec47a4cb054454e389f8e9b1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 1 Apr 2020 03:52:59 -0700
Subject: [PATCH] fix #3647

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

diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index fc7ce0837..6446c9c56 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1317,6 +1317,7 @@ namespace sat {
 
     lbool solver::do_prob_search(unsigned num_lits, literal const* lits) {
         if (m_ext) return l_undef;
+        if (num_lits > 0 || !m_user_scope_literals.empty()) return l_undef;
         SASSERT(!m_local_search);
         m_local_search = alloc(prob);
         return invoke_local_search(num_lits, lits);