From f04dfa71a6fc1431125f96c88305bd34ce8db366 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 9 Apr 2020 11:38:06 -0700
Subject: [PATCH] be a bit more graceful in failing validation #3883

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

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index a46ffaa92..42576f245 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -4585,6 +4585,10 @@ expr_ref theory_seq::elim_skolem(expr* e) {
             todo.pop_back();            
             continue;
         }
+        else if (m_util.is_skolem(a)) {
+            IF_VERBOSE(0, verbose_stream() << "unhandled skolem " << mk_pp(a, m) << "\n");
+            return expr_ref(m.mk_false(), m);
+        }
 
         args.reset();
         for (expr* arg : *to_app(a)) {