From a3844af94bf381f3e854425f09358e818a5ac664 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 24 Apr 2020 10:44:20 -0700 Subject: [PATCH] fix #4081 Signed-off-by: Nikolaj Bjorner --- src/qe/qsat.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index cdf89fa9f..b79fa60f0 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -270,7 +270,7 @@ namespace qe { bool is_boolop = (a->get_family_id() == m.get_basic_family_id()) && (!m.is_eq(a) || m.is_bool(a->get_arg(0))) && - (!m.is_distinct(a) || m.is_bool(a->get_arg(0))); + (!m.is_distinct(a) || a->get_num_args() == 0 || m.is_bool(a->get_arg(0))); if (!is_boolop && m.is_bool(a)) { TRACE("qe", tout << mk_pp(a, m) << "\n";);