From cd6496770658e3ae3cc36951f913c9831a7c8d76 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 16 May 2020 17:10:58 -0700
Subject: [PATCH] fix #4317

---
 src/cmd_context/cmd_context.cpp | 2 +-
 src/parsers/smt2/smt2parser.cpp | 7 +++----
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index efccdd434..eafc771d0 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -210,7 +210,7 @@ func_decl * func_decls::find(unsigned arity, sort * const * domain, sort * range
             if (f->get_domain(i) != domain[i])
                 break;
         }
-        if (i == arity)
+        if (i == arity || !domain)
             return f;
     }
     return nullptr;
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index b1614bc8a..085e6298a 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -1512,12 +1512,11 @@ namespace smt2 {
                 f = m_ctx.find_func_decl(C, 0, nullptr, vars.size(), nullptr, srt);
             }
             catch (cmd_exception &) {
-                if (!args.empty()) {
+                if (!vars.empty()) {
                     throw;
                 }
-            }
-            
-            if (!f && !args.empty()) {
+            }            
+            if (!f && !vars.empty()) {
                 throw parser_exception("expecting a constructor that has been declared");
             }
             if (!f) {