From f33d6f89b9dd3e298592d08a39d3b66fcf741631 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 25 Jan 2021 12:20:27 -0800
Subject: [PATCH] fix #4973

---
 src/smt/smt_setup.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index db027104e..c4fe9b05b 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -542,6 +542,8 @@ namespace smt {
         if (st.m_has_real)
             throw default_exception("Benchmark has real variables but it is marked as QF_UFLIA (uninterpreted functions and linear integer arithmetic).");
         setup_QF_UFLIA();
+        if (st.m_has_bv) 
+            setup_QF_BV();
     }
 
     void setup::setup_QF_UFLRA() {