From 899843b7cdac31fa8d0f6435f9a5f3b7c710fbe6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 26 Feb 2017 17:20:54 -0800
Subject: [PATCH] fix unhandled finite domain sort rewrite case. Issue #918

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/bv/dt2bv_tactic.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp
index 2ccbe9712..2b9cfb7f3 100644
--- a/src/tactic/bv/dt2bv_tactic.cpp
+++ b/src/tactic/bv/dt2bv_tactic.cpp
@@ -64,7 +64,10 @@ class dt2bv_tactic : public tactic {
                 return;
             }
 
-            if (m_t.is_fd(a)) {
+            if (m_t.is_fd(a) && a->get_num_args() > 0) {
+                m_t.m_non_fd_sorts.insert(get_sort(a));
+            }
+            else if (m_t.is_fd(a)) {
                 m_t.m_fd_sorts.insert(get_sort(a));
             }
             else {