Merge branch 'master' into divModSem

14 files changed, 296 insertions, 48 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 72d7b64ad..b92f767b2 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -367,6 +367,8 @@ set(regress_0_tests
   regress0/bv/mul-neg-unsat.smt2
   regress0/bv/mul-negpow2.smt2
   regress0/bv/mult-pow2-negative.smt2
+  regress0/bv/pr4993-bvugt-bvurem-a.smt2
+  regress0/bv/pr4993-bvugt-bvurem-b.smt2
   regress0/bv/sizecheck.cvc
   regress0/bv/smtcompbug.smtv1.smt2
   regress0/bv/test-bv_intro_pow2.smt2
diff --git a/test/regress/regress0/bv/ackermann2.smt2 b/test/regress/regress0/bv/ackermann2.smt2
index 3b50b025d..518faf597 100644
--- a/test/regress/regress0/bv/ackermann2.smt2
+++ b/test/regress/regress0/bv/ackermann2.smt2
@@ -1,9 +1,7 @@
 ; COMMAND-LINE: --bitblast=eager --no-check-models  --no-check-unsat-cores
 ; REQUIRES: cryptominisat
 ; REQUIRES: drat2er
-; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=lrat --no-check-unsat-cores
-; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=drat --no-check-unsat-cores
-; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=er --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_UFBV)
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/bv/core/slice-12.smtv1.smt2 b/test/regress/regress0/bv/core/slice-12.smtv1.smt2
index 3e26d9f18..d66b27caa 100644
--- a/test/regress/regress0/bv/core/slice-12.smtv1.smt2
+++ b/test/regress/regress0/bv/core/slice-12.smtv1.smt2
@@ -1,8 +1,6 @@
 ; REQUIRES: cryptominisat
 ; REQUIRES: drat2er
-; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=lrat --no-check-unsat-cores
-; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=drat --no-check-unsat-cores
-; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=er --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --no-check-unsat-cores
 ; EXPECT: unsat
 (set-option :incremental false)
 (set-info :status unsat)
diff --git a/test/regress/regress0/bv/pr4993-bvugt-bvurem-a.smt2 b/test/regress/regress0/bv/pr4993-bvugt-bvurem-a.smt2
new file mode 100644
index 000000000..c6748b19e
--- /dev/null
+++ b/test/regress/regress0/bv/pr4993-bvugt-bvurem-a.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --bv-div-zero-const --no-check-unsat-cores
+(set-logic QF_BV)
+(set-info :status unsat)
+(declare-const x (_ BitVec 4))
+(declare-const y (_ BitVec 4))
+(assert (not (= (bvugt (bvurem y x) x) (ite (= x #x0) (bvugt y #x0) false))))
+(check-sat)
diff --git a/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 b/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2
new file mode 100644
index 000000000..7cc75ef62
--- /dev/null
+++ b/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --no-bv-div-zero-const --no-check-unsat-cores
+(set-logic QF_BV)
+(set-info :status sat)
+(declare-const x (_ BitVec 4))
+(declare-const y (_ BitVec 4))
+(assert (not (= (bvugt (bvurem y x) x) (ite (= x #x0) (bvugt y #x0) false))))
+(check-sat)
diff --git a/test/regress/regress1/quantifiers/issue3481-unsat1.smt2 b/test/regress/regress1/quantifiers/issue3481-unsat1.smt2
index fb7ff5485..9cf535dc7 100644
--- a/test/regress/regress1/quantifiers/issue3481-unsat1.smt2
+++ b/test/regress/regress1/quantifiers/issue3481-unsat1.smt2
@@ -2,7 +2,7 @@
 ; EXPECT: unsat
 
 ;; produced by cvc4_16.drv ;;
-(set-logic AUFBVFPDTNIRA)
+(set-logic AUFBVDTNIRA)
 (set-info :smt-lib-version 2.6)
 ;;; generated by SMT-LIB2 driver
 ;;; SMT-LIB2 driver: bit-vectors, common part
diff --git a/test/regress/regress1/quantifiers/issue3481.smt2 b/test/regress/regress1/quantifiers/issue3481.smt2
index fe8c84d62..3d9bfe981 100644
--- a/test/regress/regress1/quantifiers/issue3481.smt2
+++ b/test/regress/regress1/quantifiers/issue3481.smt2
@@ -3,7 +3,7 @@
 
 ;; produced by cvc4_16.drv ;;
 (set-info :smt-lib-version 2.6)
-(set-logic AUFBVFPDTNIRA)
+(set-logic AUFBVDTNIRA)
 ;;; generated by SMT-LIB2 driver
 ;;; SMT-LIB2 driver: bit-vectors, common part
 ;;; SMT-LIB2: integer arithmetic
diff --git a/test/regress/regress1/sygus-abduct-test-user.smt2 b/test/regress/regress1/sygus-abduct-test-user.smt2
index bb02ebce2..ed1d5c862 100644
--- a/test/regress/regress1/sygus-abduct-test-user.smt2
+++ b/test/regress/regress1/sygus-abduct-test-user.smt2
@@ -1,3 +1,4 @@
+; REQUIRES: proof
 ; COMMAND-LINE: --produce-abducts
 ; COMMAND-LINE: --produce-abducts --sygus-core-connective
 ; SCRUBBER: grep -v -E '(\(define-fun)'
diff --git a/test/regress/regress2/bv_to_int_shifts.smt2 b/test/regress/regress2/bv_to_int_shifts.smt2
index 998234a17..d213b0c3d 100644
--- a/test/regress/regress2/bv_to_int_shifts.smt2
+++ b/test/regress/regress2/bv_to_int_shifts.smt2
@@ -1,17 +1,18 @@
 ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_BV)
-(declare-fun s () (_ BitVec 64))
-(declare-fun t () (_ BitVec 64))
-(declare-fun splust () (_ BitVec 64))
-(declare-fun shift1 () (_ BitVec 64))
-(declare-fun shift2 () (_ BitVec 64))
-(declare-fun negshift1 () (_ BitVec 64))
+(declare-fun s () (_ BitVec 4))
+(declare-fun t () (_ BitVec 4))
+(declare-fun splust () (_ BitVec 4))
+(declare-fun shift1 () (_ BitVec 4))
+(declare-fun shift2 () (_ BitVec 4))
+(declare-fun negshift1 () (_ BitVec 4))
 
 (assert (= shift1 (bvlshr s splust)))
 (assert (= shift2 (bvlshr t splust)))
 (assert (= negshift1 (bvneg shift1)))
 (assert (= splust (bvadd s t)))
 (assert (distinct negshift1 shift2))
+(assert (distinct s (bvshl s (_ bv4 4))))
 
 (check-sat)
diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py
new file mode 100644
index 000000000..a5499ffd6
--- /dev/null
+++ b/test/unit/api/python/test_datatype_api.py
@@ -0,0 +1,171 @@
+import pytest
+
+import pycvc4
+from pycvc4 import kinds
+
+
+def test_datatype_simply_rec():
+    solver = pycvc4.Solver()
+
+    # Create mutual datatypes corresponding to this definition block:
+    #
+    #   DATATYPE
+    #     wlist = leaf(data: list),
+    #     list = cons(car: wlist, cdr: list) | nil,
+    #     ns = elem(ndata: set(wlist)) | elemArray(ndata2: array(list, list))
+    #   END;
+
+    # Make unresolved types as placeholders
+    unres_wlist = solver.mkUninterpretedSort('wlist')
+    unres_list = solver.mkUninterpretedSort('list')
+    unres_ns = solver.mkUninterpretedSort('ns')
+    unres_types = set([unres_wlist, unres_list, unres_ns])
+
+    wlist = solver.mkDatatypeDecl('wlist')
+    leaf = solver.mkDatatypeConstructorDecl('leaf')
+    leaf.addSelector('data', unres_list)
+    wlist.addConstructor(leaf)
+
+    dlist = solver.mkDatatypeDecl('list')
+    cons = solver.mkDatatypeConstructorDecl('cons')
+    cons.addSelector('car', unres_wlist)
+    cons.addSelector('cdr', unres_list)
+    dlist.addConstructor(cons)
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    dlist.addConstructor(nil)
+
+    ns = solver.mkDatatypeDecl('ns')
+    elem = solver.mkDatatypeConstructorDecl('elem')
+    elem.addSelector('ndata', solver.mkSetSort(unres_wlist))
+    ns.addConstructor(elem)
+    elem_array = solver.mkDatatypeConstructorDecl('elemArray')
+    elem_array.addSelector('ndata', solver.mkArraySort(unres_list, unres_list))
+    ns.addConstructor(elem_array)
+
+    # this is well-founded and has no nested recursion
+    dtdecls = [wlist, dlist, ns]
+    dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types)
+    assert len(dtsorts) == 3
+    assert dtsorts[0].getDatatype().isWellFounded()
+    assert dtsorts[1].getDatatype().isWellFounded()
+    assert dtsorts[2].getDatatype().isWellFounded()
+    assert not dtsorts[0].getDatatype().hasNestedRecursion()
+    assert not dtsorts[1].getDatatype().hasNestedRecursion()
+    assert not dtsorts[2].getDatatype().hasNestedRecursion()
+
+    # Create mutual datatypes corresponding to this definition block:
+    #   DATATYPE
+    #     ns2 = elem2(ndata: array(int,ns2)) | nil2
+    #   END;
+    unres_ns2 = solver.mkUninterpretedSort('ns2')
+    unres_types = set([unres_ns2])
+
+    ns2 = solver.mkDatatypeDecl('ns2')
+    elem2 = solver.mkDatatypeConstructorDecl('elem2')
+    elem2.addSelector('ndata',
+                      solver.mkArraySort(solver.getIntegerSort(), unres_ns2))
+    ns2.addConstructor(elem2)
+    nil2 = solver.mkDatatypeConstructorDecl('nil2')
+    ns2.addConstructor(nil2)
+
+    # this is not well-founded due to non-simple recursion
+    dtdecls = [ns2]
+    dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types)
+    assert len(dtsorts) == 1
+    assert dtsorts[0].getDatatype()[0][0].getRangeSort().isArray()
+    elem_sort = dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort()
+    assert elem_sort == dtsorts[0]
+    assert dtsorts[0].getDatatype().isWellFounded()
+    assert dtsorts[0].getDatatype().hasNestedRecursion()
+
+    # Create mutual datatypes corresponding to this definition block:
+    #  DATATYPE
+    #    list3 = cons3(car: ns3, cdr: list3) | nil3,
+    #    ns3 = elem3(ndata: set(list3))
+    #  END
+    unres_ns3 = solver.mkUninterpretedSort('ns3')
+    unres_list3 = solver.mkUninterpretedSort('list3')
+    unres_types = set([unres_ns3, unres_list3])
+
+    list3 = solver.mkDatatypeDecl('list3')
+    cons3 = solver.mkDatatypeConstructorDecl('cons3')
+    cons3.addSelector('car', unres_ns3)
+    cons3.addSelector('cdr', unres_list3)
+    list3.addConstructor(cons3)
+    nil3 = solver.mkDatatypeConstructorDecl('nil3')
+    list3.addConstructor(nil3)
+
+    ns3 = solver.mkDatatypeDecl('ns3')
+    elem3 = solver.mkDatatypeConstructorDecl('elem3')
+    elem3.addSelector('ndata', solver.mkSetSort(unres_list3))
+    ns3.addConstructor(elem3)
+
+    # both are well-founded and have nested recursion
+    dtdecls = [list3, ns3]
+    dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types)
+    assert len(dtsorts) == 2
+    assert dtsorts[0].getDatatype().isWellFounded()
+    assert dtsorts[1].getDatatype().isWellFounded()
+    assert dtsorts[0].getDatatype().hasNestedRecursion()
+    assert dtsorts[1].getDatatype().hasNestedRecursion()
+
+    # Create mutual datatypes corresponding to this definition block:
+    #  DATATYPE
+    #    list4 = cons(car: set(ns4), cdr: list4) | nil,
+    #    ns4 = elem(ndata: list4)
+    #  END
+    unres_ns4 = solver.mkUninterpretedSort('ns4')
+    unres_list4 = solver.mkUninterpretedSort('list4')
+    unres_types = set([unres_ns4, unres_list4])
+
+    list4 = solver.mkDatatypeDecl('list4')
+    cons4 = solver.mkDatatypeConstructorDecl('cons4')
+    cons4.addSelector('car', solver.mkSetSort(unres_ns4))
+    cons4.addSelector('cdr', unres_list4)
+    list4.addConstructor(cons4)
+    nil4 = solver.mkDatatypeConstructorDecl('nil4')
+    list4.addConstructor(nil4)
+
+    ns4 = solver.mkDatatypeDecl('ns4')
+    elem4 = solver.mkDatatypeConstructorDecl('elem3')
+    elem4.addSelector('ndata', unres_list4)
+    ns4.addConstructor(elem4)
+
+    # both are well-founded and have nested recursion
+    dtdecls = [list4, ns4]
+    dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types)
+    assert len(dtsorts) == 2
+    assert dtsorts[0].getDatatype().isWellFounded()
+    assert dtsorts[1].getDatatype().isWellFounded()
+    assert dtsorts[0].getDatatype().hasNestedRecursion()
+    assert dtsorts[1].getDatatype().hasNestedRecursion()
+
+    # Create mutual datatypes corresponding to this definition block:
+    #  DATATYPE
+    #    list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil
+    #  END
+    unres_list5 = solver.mkSortConstructorSort('list5', 1)
+    unres_types = set([unres_list5])
+
+    x = solver.mkParamSort('X')
+    v = [x]
+    list5 = solver.mkDatatypeDecl('list5', v)
+
+    args = [x]
+    ur_list_x = unres_list5.instantiate(args)
+    args = [ur_list_x]
+    ur_list_list_x = unres_list5.instantiate(args)
+
+    cons5 = solver.mkDatatypeConstructorDecl('cons5')
+    cons5.addSelector('car', x)
+    cons5.addSelector('cdr', ur_list_list_x)
+    list5.addConstructor(cons5)
+    nil5 = solver.mkDatatypeConstructorDecl('nil5')
+    list5.addConstructor(nil5)
+
+    # well-founded and has nested recursion
+    dtdecls = [list5]
+    dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types)
+    assert len(dtsorts) == 1
+    assert dtsorts[0].getDatatype().isWellFounded()
+    assert dtsorts[0].getDatatype().hasNestedRecursion()
diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py
index cd40fc807..5fdb49f48 100644
--- a/test/unit/api/python/test_sort.py
+++ b/test/unit/api/python/test_sort.py
@@ -223,21 +223,31 @@ def testGetBVSize():
 
 def testGetFPExponentSize():
     solver = pycvc4.Solver()
-    fpSort = solver.mkFloatingPointSort(4, 8)
-    fpSort.getFPExponentSize()
-    setSort = solver.mkSetSort(solver.getIntegerSort())
 
-    with pytest.raises(Exception):
-        setSort.getFPExponentSize()
+    if solver.supportsFloatingPoint():
+        fpSort = solver.mkFloatingPointSort(4, 8)
+        fpSort.getFPExponentSize()
+        setSort = solver.mkSetSort(solver.getIntegerSort())
+
+        with pytest.raises(Exception):
+            setSort.getFPExponentSize()
+    else:
+        with pytest.raises(Exception):
+            solver.mkFloatingPointSort(4, 8)
 
 def testGetFPSignificandSize():
     solver = pycvc4.Solver()
-    fpSort = solver.mkFloatingPointSort(4, 8)
-    fpSort.getFPSignificandSize()
-    setSort = solver.mkSetSort(solver.getIntegerSort())
 
-    with pytest.raises(Exception):
-        setSort.getFPSignificandSize()
+    if solver.supportsFloatingPoint():
+        fpSort = solver.mkFloatingPointSort(4, 8)
+        fpSort.getFPSignificandSize()
+        setSort = solver.mkSetSort(solver.getIntegerSort())
+
+        with pytest.raises(Exception):
+            setSort.getFPSignificandSize()
+    else:
+        with pytest.raises(Exception):
+            solver.mkFloatingPointSort(4, 8)
 
 def testGetDatatypeParamSorts():
     solver = pycvc4.Solver()
diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py
index b135e4510..ca8d4c741 100644
--- a/test/unit/api/python/test_term.py
+++ b/test/unit/api/python/test_term.py
@@ -4,6 +4,17 @@ import pycvc4
 from pycvc4 import kinds
 
 
+def test_getitem():
+    solver = pycvc4.Solver()
+    intsort = solver.getIntegerSort()
+    x = solver.mkConst(intsort, 'x')
+    y = solver.mkConst(intsort, 'y')
+    xpy = solver.mkTerm(kinds.Plus, x, y)
+
+    assert xpy[0] == x
+    assert xpy[1] == y
+
+
 def test_get_kind():
     solver = pycvc4.Solver()
     intsort = solver.getIntegerSort()
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 9837d6b00..11dbbb7ae 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -27,12 +27,14 @@ class SolverBlack : public CxxTest::TestSuite
   void setUp() override;
   void tearDown() override;
 
+  void testSupportsFloatingPoint();
+
   void testGetBooleanSort();
   void testGetIntegerSort();
   void testGetNullSort();
   void testGetRealSort();
   void testGetRegExpSort();
-  void testGetRoundingmodeSort();
+  void testGetRoundingModeSort();
   void testGetStringSort();
 
   void testMkArraySort();
@@ -169,6 +171,20 @@ void SolverBlack::setUp() { d_solver.reset(new Solver()); }
 
 void SolverBlack::tearDown() { d_solver.reset(nullptr); }
 
+void SolverBlack::testSupportsFloatingPoint()
+{
+  if (d_solver->supportsFloatingPoint())
+  {
+    TS_ASSERT_THROWS_NOTHING(
+        d_solver->mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN));
+  }
+  else
+  {
+    TS_ASSERT_THROWS(d_solver->mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN),
+                     CVC4ApiException&);
+  }
+}
+
 void SolverBlack::testGetBooleanSort()
 {
   TS_ASSERT_THROWS_NOTHING(d_solver->getBooleanSort());
@@ -199,9 +215,16 @@ void SolverBlack::testGetStringSort()
   TS_ASSERT_THROWS_NOTHING(d_solver->getStringSort());
 }
 
-void SolverBlack::testGetRoundingmodeSort()
+void SolverBlack::testGetRoundingModeSort()
 {
-  TS_ASSERT_THROWS_NOTHING(d_solver->getRoundingmodeSort());
+  if (d_solver->supportsFloatingPoint())
+  {
+    TS_ASSERT_THROWS_NOTHING(d_solver->getRoundingModeSort());
+  }
+  else
+  {
+    TS_ASSERT_THROWS(d_solver->getRoundingModeSort(), CVC4ApiException&);
+  }
 }
 
 void SolverBlack::testMkArraySort()
@@ -210,15 +233,20 @@ void SolverBlack::testMkArraySort()
   Sort intSort = d_solver->getIntegerSort();
   Sort realSort = d_solver->getRealSort();
   Sort bvSort = d_solver->mkBitVectorSort(32);
-  Sort fpSort = d_solver->mkFloatingPointSort(3, 5);
   TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(boolSort, boolSort));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(intSort, intSort));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(realSort, realSort));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(bvSort, bvSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(fpSort, fpSort));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(boolSort, intSort));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(realSort, bvSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(bvSort, fpSort));
+
+  if (d_solver->supportsFloatingPoint())
+  {
+    Sort fpSort = d_solver->mkFloatingPointSort(3, 5);
+    TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(fpSort, fpSort));
+    TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(bvSort, fpSort));
+  }
+
   Solver slv;
   TS_ASSERT_THROWS(slv.mkArraySort(boolSort, boolSort), CVC4ApiException&);
 }
@@ -231,9 +259,16 @@ void SolverBlack::testMkBitVectorSort()
 
 void SolverBlack::testMkFloatingPointSort()
 {
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkFloatingPointSort(4, 8));
-  TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(0, 8), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(4, 0), CVC4ApiException&);
+  if (d_solver->supportsFloatingPoint())
+  {
+    TS_ASSERT_THROWS_NOTHING(d_solver->mkFloatingPointSort(4, 8));
+    TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(0, 8), CVC4ApiException&);
+    TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(4, 0), CVC4ApiException&);
+  }
+  else
+  {
+    TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(4, 8), CVC4ApiException&);
+  }
 }
 
 void SolverBlack::testMkDatatypeSort()
@@ -480,8 +515,16 @@ void SolverBlack::testMkBoolean()
 
 void SolverBlack::testMkRoundingMode()
 {
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver->mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO));
+  if (CVC4::Configuration::isBuiltWithSymFPU())
+  {
+    TS_ASSERT_THROWS_NOTHING(
+        d_solver->mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO));
+  }
+  else
+  {
+    TS_ASSERT_THROWS(d_solver->mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO),
+                     CVC4ApiException&);
+  }
 }
 
 void SolverBlack::testMkUninterpretedConst()
diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h
index 582a031c9..cacd92d41 100644
--- a/test/unit/theory/theory_bv_white.h
+++ b/test/unit/theory/theory_bv_white.h
@@ -15,22 +15,20 @@
  ** \todo document this file
  **/
 
-
 #include <cxxtest/TestSuite.h>
 
-#include "theory/theory.h"
+#include <vector>
+
+#include "context/context.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
-#include "theory/bv/theory_bv.h"
 #include "theory/bv/bitblast/eager_bitblaster.h"
-#include "expr/node.h"
-#include "expr/node_manager.h"
-#include "context/context.h"
-
+#include "theory/bv/bv_solver_lazy.h"
+#include "theory/theory.h"
 #include "theory/theory_test_utils.h"
 
-#include <vector>
-
 using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
@@ -76,10 +74,11 @@ public:
     // engine d_smt. We must ensure that d_smt is properly initialized via
     // the following call, which constructs its underlying theory engine.
     d_smt->finishInit();
-    EagerBitblaster* bb = new EagerBitblaster(
-        dynamic_cast<TheoryBV*>(
-            d_smt->getTheoryEngine()->d_theoryTable[THEORY_BV]),
-        d_smt->getContext());
+    TheoryBV* tbv = dynamic_cast<TheoryBV*>(
+        d_smt->getTheoryEngine()->d_theoryTable[THEORY_BV]);
+    BVSolverLazy* bvsl = dynamic_cast<BVSolverLazy*>(tbv->d_internal.get());
+    EagerBitblaster* bb = new EagerBitblaster(bvsl, d_smt->getContext());
+
     Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(16));
     Node y = d_nm->mkVar("y", d_nm->mkBitVectorType(16));
     Node x_plus_y = d_nm->mkNode(kind::BITVECTOR_PLUS, x, y);