From 057151c7a80dac44d610f5286799ad7b727b5d2c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 18 Mar 2019 07:56:25 -0700
Subject: [PATCH] fix #2188

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

diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index b9adba7cf..19e7d6ba2 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -1002,7 +1002,6 @@ void sat2goal::mc::operator()(model_ref & md) {
     // create a SAT model using md
     sat::model sat_md;
     expr_ref val(m);
-    VERIFY(!m_var2expr.empty());
     for (expr * atom : m_var2expr) {
         if (!atom) {
             sat_md.push_back(l_undef);