From a3ee7859234779181facbb2b35dbaa2f5da785e5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 21 Jun 2017 07:29:21 -0700 Subject: [PATCH] disable dt2bv for quantified variables as enum2bv does not handle them. #1092 Signed-off-by: Nikolaj Bjorner --- src/tactic/bv/dt2bv_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp index 2b9cfb7f3..cac6f1f5d 100644 --- a/src/tactic/bv/dt2bv_tactic.cpp +++ b/src/tactic/bv/dt2bv_tactic.cpp @@ -82,7 +82,7 @@ class dt2bv_tactic : public tactic { void operator()(var * v) { if (m_t.is_fd(v)) { - m_t.m_fd_sorts.insert(get_sort(v)); + m_t.m_non_fd_sorts.insert(get_sort(v)); } }