From f1193986c9cdeef45c135e65af3c0f6fcc61b083 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 26 Apr 2020 21:24:54 -0700
Subject: [PATCH] fix #4102

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/qe/qsat.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 2d8e7be01..8a9304480 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -770,6 +770,9 @@ namespace qe {
             while (!vars.empty());
             SASSERT(m_vars.back().empty()); 
             initialize_levels();
+            if (has_uninterpreted(m, fml))
+                throw tactic_exception("formula contains uninterpreted functions");
+
             TRACE("qe", tout << fml << "\n";);
         }