Merge branch 'master' into fixClangWarningsfixClangWarnings

31 files changed, 974 insertions, 379 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 816202fa9..1826b3156 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -126,6 +126,7 @@ set(regress_0_tests
   regress0/aufbv/fuzz14.smtv1.smt2
   regress0/aufbv/fuzz15.smtv1.smt2
   regress0/aufbv/issue3737.smt2
+  regress0/aufbv/issue3687-check-models-small.smt2
   regress0/aufbv/rewrite_bug.smtv1.smt2
   regress0/aufbv/try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.delta01.smtv1.smt2
   regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smtv1.smt2
@@ -584,7 +585,12 @@ set(regress_0_tests
   regress0/issue2832-qualId.smt2
   regress0/issue4010-sort-inf-var.smt2
   regress0/issue4469-unc-no-reuse-var.smt2
+  regress0/issue4707-bv-to-bool-small.smt2
+  regress0/issue5099-model-1.smt2
+  regress0/issue5099-model-2.smt2
   regress0/issue5144-resetAssertions.smt2
+  regress0/issue5540-2-dump-model.smt2
+  regress0/issue5540-model-decls.smt2
   regress0/ite.cvc
   regress0/ite2.smt2
   regress0/ite3.smt2
@@ -1016,6 +1022,7 @@ set(regress_0_tests
   regress0/strings/itos-entail.smt2
   regress0/strings/large-model.smt2
   regress0/strings/leadingzero001.smt2
+  regress0/strings/leq.smt2
   regress0/strings/loop001.smt2
   regress0/strings/loop-wrong-sem.smt2
   regress0/strings/model001.smt2
@@ -1416,6 +1423,7 @@ set(regress_1_tests
   regress1/issue3970-nl-ext-purify.smt2
   regress1/issue3990-sort-inference.smt2
   regress1/issue4273-ext-rew-cache.smt2
+  regress1/issue4335-unsat-core.smt2
   regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2
   regress1/lemmas/pursuit-safety-8.smtv1.smt2
   regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
@@ -1622,6 +1630,8 @@ set(regress_1_tests
   regress1/quantifiers/issue5482-rtf-no-fv.smt2
   regress1/quantifiers/issue5484-qe.smt2
   regress1/quantifiers/issue5484b-qe.smt2
+  regress1/quantifiers/issue5506-qe.smt2
+  regress1/quantifiers/issue5507-qe.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lia-witness-div-pp.smt2
@@ -2167,6 +2177,8 @@ set(regress_2_tests
   regress2/hole7.cvc
   regress2/hole8.cvc
   regress2/instance_1444.smtv1.smt2
+  regress2/issue3687-check-models.smt2
+  regress2/issue4707-bv-to-bool-large.smt2
   regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2
   regress2/javafe.ast.WhileStmt.447_no_forall.smt2
   regress2/ooo.rf6.smt2
diff --git a/test/regress/regress0/aufbv/issue3687-check-models-small.smt2 b/test/regress/regress0/aufbv/issue3687-check-models-small.smt2
new file mode 100644
index 000000000..88cbd8a0b
--- /dev/null
+++ b/test/regress/regress0/aufbv/issue3687-check-models-small.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --check-models
+; EXPECT: sat
+(set-logic QF_AUFBV)
+(declare-fun a () (Array (_ BitVec 2) (_ BitVec 2)))
+(declare-fun b () (_ BitVec 2))
+(assert (distinct #b01 (select (store (store a #b01 (bvor #b01 (select a
+  #b00))) #b10 #b00) b)))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/bv/bv_to_int_5281.smt2 b/test/regress/regress0/bv/bv_to_int_5281.smt2
index 4d0da1dbb..dc2cb7f35 100644
--- a/test/regress/regress0/bv/bv_to_int_5281.smt2
+++ b/test/regress/regress0/bv/bv_to_int_5281.smt2
@@ -1,4 +1,4 @@
-; COMMAND: --check-models --incremental
+; COMMAND-LINE: --check-models --incremental
 ; EXPECT: sat
 (set-logic ALL)
 (set-option :check-models true)
diff --git a/test/regress/regress0/issue4707-bv-to-bool-small.smt2 b/test/regress/regress0/issue4707-bv-to-bool-small.smt2
new file mode 100644
index 000000000..c2f0a58ad
--- /dev/null
+++ b/test/regress/regress0/issue4707-bv-to-bool-small.smt2
@@ -0,0 +1,13 @@
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun b () (Array (_ BitVec 10) (_ BitVec 1)))
+(declare-fun c () (Array (_ BitVec 10) (_ BitVec 1)))
+(declare-fun ae () (_ BitVec 10))
+(declare-fun ag () (_ BitVec 10))
+(declare-fun ak () (_ BitVec 10))
+(assert (= (_ bv1 1) (bvand (bvcomp ae ((_ zero_extend 9) (select b (_ bv0
+  10)))) (bvsdiv (bvcomp ae ak) (bvand (ite (= (_ bv0 1) (bvcomp ag (bvshl ((_
+  zero_extend 9) (select c (bvadd ae (_ bv3 10)))) (_ bv8 10)))) (_ bv1 1) (_
+  bv0 1)) (ite (= b (store (store c (bvadd ae (_ bv3 10)) ((_ extract 0 0)
+  (bvlshr ag (_ bv8 10)))) ak (_ bv1 1))) (_ bv1 1) (_ bv0 1)))))))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/issue5099-model-1.smt2 b/test/regress/regress0/issue5099-model-1.smt2
new file mode 100644
index 000000000..dd422ab3b
--- /dev/null
+++ b/test/regress/regress0/issue5099-model-1.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: -m
+; EXPECT: sat
+; EXPECT: ((baz true))
+(set-logic QF_NIRA)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(assert (! (or (= a (div 0 b))) :named baz))
+(assert (and (> b 5)))
+(check-sat)
+(get-assignment)
diff --git a/test/regress/regress0/issue5099-model-2.smt2 b/test/regress/regress0/issue5099-model-2.smt2
new file mode 100644
index 000000000..2bd27093f
--- /dev/null
+++ b/test/regress/regress0/issue5099-model-2.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: -m
+; EXPECT: sat
+; EXPECT: ((IP true))
+(set-logic QF_NRA)
+(declare-const r11 Real)
+(declare-const r16 Real)
+(assert (! (distinct (/ 1 r16) r11) :named IP))
+(check-sat)
+(get-assignment)
\ No newline at end of file
diff --git a/test/regress/regress0/issue5540-2-dump-model.smt2 b/test/regress/regress0/issue5540-2-dump-model.smt2
new file mode 100644
index 000000000..56d3b2458
--- /dev/null
+++ b/test/regress/regress0/issue5540-2-dump-model.smt2
@@ -0,0 +1,9 @@
+; SCRUBBER: sed -e 's/Bool.*$/Bool/'
+; COMMAND-LINE: --dump-models
+; EXPECT: sat
+; EXPECT: (
+; EXPECT: (define-fun v16 () Bool
+; EXPECT: )
+(set-logic UFLIA)
+(declare-fun v16 () Bool)
+(check-sat)
diff --git a/test/regress/regress0/issue5540-model-decls.smt2 b/test/regress/regress0/issue5540-model-decls.smt2
new file mode 100644
index 000000000..714159c9f
--- /dev/null
+++ b/test/regress/regress0/issue5540-model-decls.smt2
@@ -0,0 +1,19 @@
+; SCRUBBER: sed -e 's/Bool.*$/Bool/'
+; COMMAND-LINE: --dump-models -i
+; EXPECT:sat
+; EXPECT: (
+; EXPECT: (define-fun a () Bool
+; EXPECT: )
+; EXPECT: sat
+; EXPECT: (
+; EXPECT: (define-fun a () Bool
+; EXPECT: )
+; EXPECT: sat
+; EXPECT: (
+; EXPECT: (define-fun a () Bool
+; EXPECT: )
+(set-logic ALL)
+(declare-fun a () Bool)
+(check-sat)
+(check-sat)
+(check-sat)
diff --git a/test/regress/regress0/strings/leq.smt2 b/test/regress/regress0/strings/leq.smt2
new file mode 100644
index 000000000..b3bd40739
--- /dev/null
+++ b/test/regress/regress0/strings/leq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --strings-exp
+(set-logic QF_SLIA)
+(declare-const x String)
+(declare-const y String)
+(assert (or
+  (not (str.<= (str.++ "A" x) (str.++ "B" y)))
+  (not (str.<= (str.++ "A" x) (str.++ "BC" y)))
+  (str.<= (str.++ "A" "D" x) (str.++ "AC" y))))
+(set-info :status unsat)
+(check-sat)
diff --git a/test/regress/regress1/issue4335-unsat-core.smt2 b/test/regress/regress1/issue4335-unsat-core.smt2
new file mode 100644
index 000000000..11e689515
--- /dev/null
+++ b/test/regress/regress1/issue4335-unsat-core.smt2
@@ -0,0 +1,187 @@
+; SCRUBBER: sed -e 's/IP_[0-9]*/IP/'
+; EXPECT: unsat
+; EXPECT: (
+; EXPECT: IP
+; EXPECT: IP
+; EXPECT: IP
+; EXPECT: IP
+; EXPECT: IP
+; EXPECT: IP
+; EXPECT: IP
+; EXPECT: IP
+; EXPECT: IP
+; EXPECT: )
+(set-logic ALL)
+(set-option :produce-unsat-cores true)
+(declare-const v0 Bool)
+(declare-const v1 Bool)
+(declare-const v2 Bool)
+(declare-const v3 Bool)
+(declare-const v4 Bool)
+(declare-const i1 Int)
+(declare-const r1 Real)
+(declare-const r2 Real)
+(declare-const r3 Real)
+(declare-const r7 Real)
+(declare-const r10 Real)
+(declare-const r14 Real)
+(declare-const r16 Real)
+(declare-const r17 Real)
+(declare-const r18 Real)
+(declare-const v5 Bool)
+(declare-const r20 Real)
+(declare-const arr-5074471134850140881_778238581772319464-0 (Array Bool Int))
+(assert (! (exists ((q0 Int) (q1 Real) (q2 Int)) (not (> (- i1) (select (store arr-5074471134850140881_778238581772319464-0 v0 60) (= v0 v4 v3 v3 v4))))) :named IP_1))
+(assert (! (or (forall ((q0 Int) (q1 Real) (q2 Int)) (=> (>= r20 q1 q1 26271062.0) (<= q2 q2))) (exists ((q0 Int) (q1 Real) (q2 Int)) (=> (>= (- i1) q2) (< q1 q1 5851734.0)))) :named IP_2))
+(declare-const arr-778238581772319464_-3713212254555730767-0 (Array Int (_ BitVec 8)))
+(declare-const v6 Bool)
+(declare-const v7 Bool)
+(declare-const arr--5101604640448673848_-3713212254554648242-0 (Array Real (_ BitVec 9)))
+(declare-const arr--3713212254557895817_-5101604640448673848-0 (Array (_ BitVec 10) Real))
+(assert (! (or (distinct (- i1) 35) (not v4) (= v0 v4 v3 v3 v4)) :named IP_3))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v0 (= v0 v4 v3 v3 v4)) :named IP_4))
+(assert (! (or (= v0 v4 v3 v3 v4) (distinct v4 (= v0 v4 v3 v3 v4)) (not v4)) :named IP_5))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 (= v0 v4 v3 v3 v4)) :named IP_6))
+(assert (! (or (= v0 v4 v3 v3 v4) v3 (= v0 v4 v3 v3 v4)) :named IP_7))
+(assert (! (or (is_int 1193124502.0) (= v0 v4 v3 v3 v4) (not v4)) :named IP_8))
+(assert (! (or (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4) v0) :named IP_9))
+(assert (! (or (< 397 (div (- i1) 60)) v3 (= v0 v4 v3 v3 v4)) :named IP_10))
+(assert (! (or v3 v3 v3) :named IP_11))
+(assert (! (or (is_int 1193124502.0) (not v4) (= v0 v4 v3 v3 v4)) :named IP_12))
+(assert (! (or (< 397 (div (- i1) 60)) (is_int 1193124502.0) (distinct (- i1) 35)) :named IP_13))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) v0) :named IP_14))
+(assert (! (or (is_int 1193124502.0) v0 (not v4)) :named IP_15))
+(assert (! (or (< 397 (div (- i1) 60)) (< 397 (div (- i1) 60)) (< 397 (div (- i1) 60))) :named IP_16))
+(assert (! (or (not v4) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35)) :named IP_17))
+(assert (! (or (distinct (- i1) 35) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_18))
+(assert (! (or v3 (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_19))
+(assert (! (or (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4) (is_int 1193124502.0)) :named IP_20))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_21))
+(assert (! (or (< 397 (div (- i1) 60)) (distinct (- i1) 35) (= v0 v4 v3 v3 v4)) :named IP_22))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 (is_int 1193124502.0)) :named IP_23))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) (= v0 v4 v3 v3 v4)) :named IP_24))
+(assert (! (or (= v0 v4 v3 v3 v4) (is_int 1193124502.0) (< 397 (div (- i1) 60))) :named IP_25))
+(assert (! (or v0 v0 (= v0 v4 v3 v3 v4)) :named IP_26))
+(assert (! (or v0 (not v4) (= v0 v4 v3 v3 v4)) :named IP_27))
+(assert (! (or (= v0 v4 v3 v3 v4) v3 v3) :named IP_28))
+(assert (! (or v3 (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_29))
+(assert (! (or (is_int 1193124502.0) (is_int 1193124502.0) (distinct (- i1) 35)) :named IP_30))
+(assert (! (or (distinct (- i1) 35) (not v4) (distinct (- i1) 35)) :named IP_31))
+(assert (! (or (= v0 v4 v3 v3 v4) (< 397 (div (- i1) 60)) v3) :named IP_32))
+(assert (! (or (= v0 v4 v3 v3 v4) (distinct (- i1) 35) (not v4)) :named IP_33))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v0 v0) :named IP_34))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) (< 397 (div (- i1) 60))) :named IP_35))
+(assert (! (or (= v0 v4 v3 v3 v4) (is_int 1193124502.0) (not v4)) :named IP_36))
+(assert (! (or (= v0 v4 v3 v3 v4) (distinct (- i1) 35) v0) :named IP_37))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (< 397 (div (- i1) 60)) (< 397 (div (- i1) 60))) :named IP_38))
+(assert (! (or (distinct (- i1) 35) v3 (= v0 v4 v3 v3 v4)) :named IP_39))
+(assert (! (or (< 397 (div (- i1) 60)) (is_int 1193124502.0) (not v4)) :named IP_40))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 (is_int 1193124502.0)) :named IP_41))
+(assert (! (or v0 (distinct (- i1) 35) v0) :named IP_42))
+(assert (! (or (not v4) v0 (not v4)) :named IP_43))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (not v4) (= v0 v4 v3 v3 v4)) :named IP_44))
+(assert (! (or (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4)) (is_int 1193124502.0)) :named IP_45))
+(assert (! (or v0 (is_int 1193124502.0) (distinct (- i1) 35)) :named IP_46))
+(assert (! (or (= v0 v4 v3 v3 v4) v0 (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_47))
+(assert (! (or (is_int 1193124502.0) v0 (= v0 v4 v3 v3 v4)) :named IP_48))
+(assert (! (or v0 (< 397 (div (- i1) 60)) v3) :named IP_49))
+(assert (! (or v0 v3 (is_int 1193124502.0)) :named IP_50))
+(assert (! (or v3 (distinct (- i1) 35) v0) :named IP_51))
+(assert (! (or v3 (distinct v4 (= v0 v4 v3 v3 v4)) (is_int 1193124502.0)) :named IP_52))
+(assert (! (or (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4)) (not v4)) :named IP_53))
+(assert (! (or (= v0 v4 v3 v3 v4) (< 397 (div (- i1) 60)) (distinct (- i1) 35)) :named IP_54))
+(assert (! (or (distinct (- i1) 35) v3 (not v4)) :named IP_55))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) v0) :named IP_56))
+(assert (! (or (= v0 v4 v3 v3 v4) (< 397 (div (- i1) 60)) (distinct (- i1) 35)) :named IP_57))
+(assert (! (or (not v4) v0 (< 397 (div (- i1) 60))) :named IP_58))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) (not v4)) :named IP_59))
+(assert (! (or (= v0 v4 v3 v3 v4) (distinct (- i1) 35) (is_int 1193124502.0)) :named IP_60))
+(assert (! (or (is_int 1193124502.0) v0 (distinct (- i1) 35)) :named IP_61))
+(assert (! (or (not v4) (< 397 (div (- i1) 60)) v3) :named IP_62))
+(assert (! (or (not v4) (distinct (- i1) 35) v0) :named IP_63))
+(assert (! (or (distinct (- i1) 35) (is_int 1193124502.0) v3) :named IP_64))
+(assert (! (or (= v0 v4 v3 v3 v4) (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4)) :named IP_65))
+(assert (! (or (< 397 (div (- i1) 60)) v3 v3) :named IP_66))
+(assert (! (or (not v4) v3 (distinct (- i1) 35)) :named IP_67))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 v3) :named IP_68))
+(assert (! (or (distinct (- i1) 35) (distinct (- i1) 35) v0) :named IP_69))
+(assert (! (or v3 (not v4) (< 397 (div (- i1) 60))) :named IP_70))
+(assert (! (or (< 397 (div (- i1) 60)) (is_int 1193124502.0) (< 397 (div (- i1) 60))) :named IP_71))
+(assert (! (or (< 397 (div (- i1) 60)) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_72))
+(assert (! (or (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4)) (not v4)) :named IP_73))
+(assert (! (or v0 v0 (is_int 1193124502.0)) :named IP_74))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_75))
+(assert (! (or v3 (not v4) v0) :named IP_76))
+(assert (! (or (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4)) (not v4)) :named IP_77))
+(assert (! (or v3 (is_int 1193124502.0) (< 397 (div (- i1) 60))) :named IP_78))
+(assert (! (or (is_int 1193124502.0) (not v4) v0) :named IP_79))
+(assert (! (or (not v4) v3 (not v4)) :named IP_80))
+(assert (! (or v3 v0 v0) :named IP_81))
+(assert (! (or (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4) (is_int 1193124502.0)) :named IP_82))
+(assert (! (or (is_int 1193124502.0) (= v0 v4 v3 v3 v4) (not v4)) :named IP_83))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (is_int 1193124502.0) v0) :named IP_84))
+(assert (! (or (not v4) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_85))
+(assert (! (or (= v0 v4 v3 v3 v4) v0 (= v0 v4 v3 v3 v4)) :named IP_86))
+(assert (! (or v3 (distinct (- i1) 35) (not v4)) :named IP_87))
+(assert (! (or (distinct (- i1) 35) v0 (not v4)) :named IP_88))
+(assert (! (or (distinct (- i1) 35) (< 397 (div (- i1) 60)) (distinct (- i1) 35)) :named IP_89))
+(assert (! (or (distinct (- i1) 35) (< 397 (div (- i1) 60)) (not v4)) :named IP_90))
+(assert (! (or (= v0 v4 v3 v3 v4) (is_int 1193124502.0) (distinct (- i1) 35)) :named IP_91))
+(assert (! (or (is_int 1193124502.0) (< 397 (div (- i1) 60)) (distinct (- i1) 35)) :named IP_92))
+(assert (! (or v0 (distinct (- i1) 35) (is_int 1193124502.0)) :named IP_93))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) (= v0 v4 v3 v3 v4)) :named IP_94))
+(assert (! (or (= v0 v4 v3 v3 v4) (distinct (- i1) 35) (= v0 v4 v3 v3 v4)) :named IP_95))
+(assert (! (or v3 (not v4) (is_int 1193124502.0)) :named IP_96))
+(assert (! (or (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_97))
+(assert (! (or (= v0 v4 v3 v3 v4) v3 (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_98))
+(assert (! (or (distinct (- i1) 35) (distinct v4 (= v0 v4 v3 v3 v4)) v3) :named IP_99))
+(assert (! (or v0 v0 (= v0 v4 v3 v3 v4)) :named IP_100))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_101))
+(assert (! (or (is_int 1193124502.0) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_102))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4)) :named IP_103))
+(assert (! (or (not v4) (not v4) (= v0 v4 v3 v3 v4)) :named IP_104))
+(assert (! (or (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35)) :named IP_105))
+(assert (! (or (= v0 v4 v3 v3 v4) (< 397 (div (- i1) 60)) (is_int 1193124502.0)) :named IP_106))
+(assert (! (or v0 (is_int 1193124502.0) (distinct (- i1) 35)) :named IP_107))
+(assert (! (or (< 397 (div (- i1) 60)) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_108))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 (distinct (- i1) 35)) :named IP_109))
+(assert (! (or (= v0 v4 v3 v3 v4) v0 (not v4)) :named IP_110))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4) (is_int 1193124502.0)) :named IP_111))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4) (distinct (- i1) 35)) :named IP_112))
+(assert (! (or v0 (not v4) (< 397 (div (- i1) 60))) :named IP_113))
+(assert (! (or v3 (distinct (- i1) 35) v0) :named IP_114))
+(assert (! (or (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_115))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35)) :named IP_116))
+(assert (! (or (< 397 (div (- i1) 60)) (is_int 1193124502.0) (not v4)) :named IP_117))
+(assert (! (or v0 (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_118))
+(assert (! (or (distinct (- i1) 35) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_119))
+(assert (! (or (= v0 v4 v3 v3 v4) (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_120))
+(assert (! (or v3 v3 v3) :named IP_121))
+(assert (! (or (is_int 1193124502.0) (< 397 (div (- i1) 60)) v3) :named IP_122))
+(assert (! (or (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_123))
+(assert (! (or (not v4) (= v0 v4 v3 v3 v4) v3) :named IP_124))
+(assert (! (or (distinct (- i1) 35) (< 397 (div (- i1) 60)) (< 397 (div (- i1) 60))) :named IP_125))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) (not v4)) :named IP_126))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v0 v0) :named IP_127))
+(assert (! (or (is_int 1193124502.0) (distinct (- i1) 35) (is_int 1193124502.0)) :named IP_128))
+(assert (! (or v0 (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_129))
+(assert (! (or v0 (distinct (- i1) 35) v0) :named IP_130))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4) (is_int 1193124502.0)) :named IP_131))
+(assert (! (or (not v4) v3 (distinct (- i1) 35)) :named IP_132))
+(assert (! (or v0 (< 397 (div (- i1) 60)) (= v0 v4 v3 v3 v4)) :named IP_133))
+(assert (! (or (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4)) (< 397 (div (- i1) 60))) :named IP_134))
+(assert (! (or v0 (distinct v4 (= v0 v4 v3 v3 v4)) (is_int 1193124502.0)) :named IP_135))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_136))
+(assert (! (or v3 (= v0 v4 v3 v3 v4) (< 397 (div (- i1) 60))) :named IP_137))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 (distinct (- i1) 35)) :named IP_138))
+(assert (! (or v3 (< 397 (div (- i1) 60)) (distinct (- i1) 35)) :named IP_139))
+(assert (! (or (< 397 (div (- i1) 60)) (< 397 (div (- i1) 60)) v3) :named IP_140))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (< 397 (div (- i1) 60)) v0) :named IP_141))
+(assert (! (or (< 397 (div (- i1) 60)) (not v4) v3) :named IP_142))
+(assert (! (or (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35)) :named IP_143))
+(assert (! (or v3 (is_int 1193124502.0) v3) :named IP_144))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v0 (< 397 (div (- i1) 60))) :named IP_145))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (not v4) v3) :named IP_146))
+(check-sat-assuming (IP_107 IP_133))
+(get-unsat-core)
+(exit)
\ No newline at end of file
diff --git a/test/regress/regress1/quantifiers/issue5506-qe.smt2 b/test/regress/regress1/quantifiers/issue5506-qe.smt2
new file mode 100644
index 000000000..3839f2d75
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5506-qe.smt2
@@ -0,0 +1,6 @@
+; SCRUBBER: sed 's/(.*)/()/g'
+; EXPECT: ()
+; EXIT: 0
+(set-logic LIA)
+(declare-fun a () Int)
+(get-qe (forall ((b Int)) (= a 0)))
diff --git a/test/regress/regress1/quantifiers/issue5507-qe.smt2 b/test/regress/regress1/quantifiers/issue5507-qe.smt2
new file mode 100644
index 000000000..3b7ddbcf3
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5507-qe.smt2
@@ -0,0 +1,19 @@
+; EXPECT: false
+; EXIT: 0
+(set-logic LIA)
+(declare-fun v0 () Bool)
+(declare-fun v1 () Bool)
+(declare-fun v2 () Bool)
+(declare-fun v3 () Bool)
+(declare-fun v5 () Bool)
+(declare-fun v6 () Bool)
+(declare-fun v9 () Bool)
+(declare-fun v10 () Bool)
+(declare-fun v15 () Bool)
+(declare-fun v16 () Bool)
+(declare-fun i0 () Int)
+(declare-fun i2 () Int)
+(declare-fun i9 () Int)
+(declare-fun v26 () Bool)
+(declare-fun v33 () Bool)
+(get-qe (exists ((q154 Bool) (q155 Int) (q156 Bool) (q157 Bool) (q158 Bool) (q159 Bool) (q160 Int)) (and (=> (distinct 309 i2) (or q157 v9 (distinct v16 v6 v5 v10) q159 (=> v15 v26))) (exists ((q154 Bool) (q155 Int) (q156 Bool) (q157 Bool) (q158 Bool) (q159 Bool) (q160 Int)) (=> (xor q156 v3 v2 q156 q156 q159 (>= 217 826 149 i0 i9) v1 v5 q157 q157) (distinct q160 q160))) v33 (distinct v16 v6 v5 v10) v0)))
diff --git a/test/regress/regress2/issue3687-check-models.smt2 b/test/regress/regress2/issue3687-check-models.smt2
new file mode 100644
index 000000000..02f7754cf
--- /dev/null
+++ b/test/regress/regress2/issue3687-check-models.smt2
@@ -0,0 +1,51 @@
+; COMMAND-LINE: --check-models
+; EXPECT: sat
+(set-logic QF_ABV)
+(declare-fun c () (_ BitVec 32))
+(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
+(declare-fun b () (_ BitVec 32))
+(assert (let ((a!1 (bvxnor (concat #x000000 (select a (bvadd c #x00000001))) #x00000008))
+      (a!3 (bvsdiv (concat #x000000 (select a (bvadd c #x00000002))) #x00000010))
+      (a!4 (bvudiv (concat #x000000 (select a (bvashr c #x00000003)))
+                   #x00000018))
+      (a!5 (select a
+                   (bvxor (bvsub (bvnand c #x00000004) #x00000004) #x00000000)))
+      (a!6 (select a
+                   (bvsdiv (bvsub (bvnand c #x00000004) #x00000004) #x00000001)))
+      (a!7 (select a
+                   (bvadd (bvsub (bvnand c #x00000004) #x00000004) #x00000002)))
+      (a!9 (store a
+                  (bvashr (bvurem (bvnand c #x00000004) #x00000004) #x00000001)
+                  ((_ extract 7 0) (bvxnor b #x00000008))))
+      (a!11 (bvnand (bvurem (bvsub (bvnand c #x00000004) #x00000004) #x00000004)
+                    #x00000008)))
+(let ((a!2 (bvnor (concat #x000000 (select a (bvsmod c #x00000000))) a!1))
+      (a!8 (bvlshr (bvor (concat #x000000 a!5)
+                         (bvmul (concat #x000000 a!6) #x00000008))
+                   (bvand (concat #x000000 a!7) #x00000010)))
+      (a!10 (store a!9
+                   (bvshl (bvurem (bvnand c #x00000004) #x00000004) #x00000000)
+                   ((_ extract 7 0) b)))
+      (a!12 (bvsub (concat #x000000 (select a (bvashr a!11 #x00000001)))
+                   #x00000008))
+      (a!14 (bvxnor (concat #x000000 (select a (bvxnor a!11 #x00000002)))
+                    #x00000010))
+      (a!15 (bvxor (concat #x000000 (select a (bvsub a!11 #x00000003)))
+                   #x00000018)))
+(let ((a!13 (bvor (concat #x000000 (select a (bvmul a!11 #x00000000))) a!12)))
+(let ((a!16 ((_ extract 7 0)
+              (bvmul (bvurem (bvurem a!13 a!14) a!15) #x00000018)))
+      (a!17 ((_ extract 7 0) (bvor (bvurem (bvurem a!13 a!14) a!15) #x00000010)))
+      (a!18 ((_ extract 7 0)
+              (bvnor (bvurem (bvurem a!13 a!14) a!15) #x00000008))))
+(let ((a!19 (store (store (store (store a!10 #x08053e77 a!16) #x08053e76 a!17)
+                          #x08053e75
+                          a!18)
+                   #x08053e74
+                   ((_ extract 7 0) (bvurem (bvurem a!13 a!14) a!15)))))
+(let ((a!20 (select a!19
+                    (bvadd (bvsub (bvnand c #x00000004) #x00000004) #x00000003))))
+(let ((a!21 (distinct (bvsdiv (bvsmod a!2 a!3) a!4)
+                      (bvshl a!8 (bvshl (concat #x000000 a!20) #x00000018)))))
+  (= #b1 (bvashr (ite (or a!21) #b1 #b0) #b1))))))))))
+(check-sat)
diff --git a/test/regress/regress2/issue4707-bv-to-bool-large.smt2 b/test/regress/regress2/issue4707-bv-to-bool-large.smt2
new file mode 100644
index 000000000..bb4e9794c
--- /dev/null
+++ b/test/regress/regress2/issue4707-bv-to-bool-large.smt2
@@ -0,0 +1,129 @@
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
+(declare-fun b () (Array (_ BitVec 32) (_ BitVec 8)))
+(declare-fun c () (Array (_ BitVec 32) (_ BitVec 8)))
+(declare-fun d () (Array (_ BitVec 32) (_ BitVec 8)))
+(declare-fun aa () (_ BitVec 1))
+(declare-fun e () (_ BitVec 1))
+(declare-fun f () (_ BitVec 1))
+(declare-fun ab () (_ BitVec 1))
+(declare-fun g () (_ BitVec 1))
+(declare-fun h () (_ BitVec 1))
+(declare-fun i () (_ BitVec 1))
+(declare-fun j () (_ BitVec 1))
+(declare-fun k () (_ BitVec 1))
+(declare-fun l () (_ BitVec 1))
+(declare-fun m () (_ BitVec 1))
+(declare-fun n () (_ BitVec 1))
+(declare-fun o () (_ BitVec 1))
+(declare-fun p () (_ BitVec 1))
+(declare-fun q () (_ BitVec 1))
+(declare-fun r () (_ BitVec 1))
+(declare-fun s () (_ BitVec 1))
+(declare-fun t () (_ BitVec 1))
+(declare-fun u () (_ BitVec 1))
+(declare-fun v () (_ BitVec 1))
+(declare-fun w () (_ BitVec 1))
+(declare-fun x () (_ BitVec 1))
+(declare-fun y () (_ BitVec 1))
+(declare-fun z () (_ BitVec 1))
+(declare-fun ac () (_ BitVec 1))
+(declare-fun ad () (_ BitVec 32))
+(declare-fun ae () (_ BitVec 32))
+(declare-fun af () (_ BitVec 32))
+(declare-fun ag () (_ BitVec 32))
+(declare-fun ah () (_ BitVec 32))
+(declare-fun ai () (_ BitVec 32))
+(declare-fun aj () (_ BitVec 32))
+(declare-fun ak () (_ BitVec 32))
+(declare-fun al () (_ BitVec 32))
+(declare-fun am () (_ BitVec 32))
+(declare-fun an () (_ BitVec 32))
+(declare-fun ao () (_ BitVec 1))
+(declare-fun ap () (_ BitVec 32))
+(declare-fun aq () (_ BitVec 1))
+(declare-fun ar () (_ BitVec 32))
+(declare-fun au () (_ BitVec 32))
+(declare-fun av () (_ BitVec 32))
+(declare-fun aw () (_ BitVec 32))
+(declare-fun ax () (_ BitVec 32))
+(declare-fun ay () (_ BitVec 32))
+(assert
+ (let ((?as (bvadd av (_ bv4 32)))
+    (?at (bvadd av (_ bv12 32))))
+  (= (_ bv1 1) (bvand (bvand (ite (= ac (ite (= an ai) (_ bv1 1) (_
+  bv0 1))) (_ bv1 1) (_ bv0 1)) (bvmul (ite (= z (ite (= ai aj) (_
+  bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= y (ite (= aj
+  (bvor (bvnand (bvor (concat (_ bv0 24) (select d (bvadd ak (_ bv0
+  32)))) (bvshl (concat (_ bv0 24) (select d (bvadd ak (_ bv1 32))))
+  (_ bv8 32))) (bvshl (concat (_ bv0 24) (select d (bvadd ak (_ bv2
+  32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select d (bvadd ak
+  (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0
+  1)) (bvand (ite (= x (ite (= ak ?as) (_ bv1 1) (_ bv0 1))) (_ bv1
+  1) (_ bv0 1)) (bvand (ite (= w (ite (= d (store (store (store
+  (store c (bvadd (_ bv134533664 32) (_ bv3 32)) ((_ extract 7 0)
+  (bvlshr al (_ bv24 32)))) (bvadd (_ bv134533664 32) (_ bv2 32)) ((_
+  extract 7 0) (bvlshr al (_ bv16 32)))) (bvadd (_ bv134533664 32) (_
+  bv1 32)) ((_ extract 7 0) (bvlshr al (_ bv8 32)))) (bvadd (_
+  bv134533664 32) (_ bv0 32)) ((_ extract 7 0) al))) (_ bv1 1) (_ bv0
+  1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= v (ite (= al (bvor (bvor
+  (bvor (concat (_ bv0 24) (select c (bvadd am (_ bv0 32)))) (bvshl
+  (concat (_ bv0 24) (select c (bvadd am (_ bv1 32)))) (_ bv8 32)))
+  (bvshl (concat (_ bv0 24) (select c (bvadd am (_ bv2 32)))) (_ bv16
+  32))) (bvshl (concat (_ bv0 24) (select c (bvsub am (_ bv3 32))))
+  (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand
+  (ite (= u (ite (= am ?at) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0
+  1)) (bvand (ite (= t ao) (_ bv1 1) (_ bv0 1)) (bvand (ite (= s (ite
+  (= an ad) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (=
+  r (ite (= ad ae) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand
+  (ite (= q (ite (= ae (bvor (bvor (bvor (concat (_ bv0 24) (select b
+  (bvadd af (_ bv0 32)))) (bvxor (concat (_ bv0 24) (select b (bvadd
+  af (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select b
+  (bvadd af (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24)
+  (select b (bvadd af (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0
+  1))) (_ bv1 1) (_ bv0 1)) (bvsdiv (ite (= p (ite (= af ?as) (_ bv1
+  1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= o (ite (= b
+  (store (store (store (store c (bvadd ar (_ bv3 32)) ((_ extract 7
+  0) (bvlshr ag (_ bv24 32)))) (bvadd ar (_ bv2 32)) ((_ extract 7 0)
+  (bvlshr ag (_ bv16 32)))) (bvand ar (_ bv1 32)) ((_ extract 7 0)
+  (bvlshr ag (_ bv8 32)))) (bvadd ar (_ bv0 32)) ((_ extract 7 0)
+  ag))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= n
+  (ite (= ag (bvor (bvor (bvor (concat (_ bv0 24) (select c (bvadd ah
+  (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select c (bvadd ah (_ bv1
+  32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select c (bvurem ah
+  (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select c
+  (bvadd ah (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1
+  1) (_ bv0 1)) (bvand (ite (= m (ite (= ah ?at) (_ bv1 1) (_ bv0
+  1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= l ao ) (_ bv1 1) (_ bv0
+  1)) (bvand (ite (= k (bvor (bvand t (bvand u (bvand v (bvand w
+  (bvand x (bvand y (bvand z ac))))))) (bvand l (bvand m (bvand n
+  (bvand o (bvand p (bvand q (bvand r s))))))))) (_ bv1 1) (_ bv0 1))
+  (bvand (ite (= j (ite (= ao ((_ extract 0 0) ap)) (_ bv1 1) (_ bv0
+  1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= i (ite (= ap (concat (_
+  bv0 31) aq)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite
+  (= h (ite (= aq (ite (= ar (_ bv0 32)) (_ bv1 1) (_ bv0 1))) (_ bv1
+  1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= g (ite (= ar
+  (bvor (bvor (bvor (concat (_ bv0 24) (select c (bvadd au (_ bv0
+  32)))) (bvshl (concat (_ bv0 24) (select c (bvadd au (_ bv1 32))))
+  (_ bv8 32))) (bvshl (concat (_ bv0 24) (select c (bvadd au (_ bv2
+  32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select c (bvadd au
+  (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0
+  1)) (bvand (ite (= ab (ite (= au (bvadd av (_ bv8 32))) (_ bv1 1)
+  (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= f (ite (= c (store
+  (store (store (store a (bvadd av (_ bv3 32)) ((_ extract 7 0)
+  (bvlshr ay (_ bv24 32)))) (bvadd av (_ bv2 32)) ((_ extract 7 0)
+  (bvlshr ay (_ bv16 32)))) (bvadd av (_ bv1 32)) ((_ extract 7 0)
+  (bvlshr ay (_ bv8 32)))) (bvadd av (_ bv0 32)) ((_ extract 7 0)
+  ay))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= e
+  (ite (= av (bvsub ax (_ bv4 32))) (_ bv1 1) (_ bv0 1))) (_ bv1 1)
+  (_ bv0 1)) (ite (= aa (ite (= aw (bvor (bvor (bvor (concat (_ bv0
+  24) (select a (bvadd ax (_ bv0 32)))) (bvshl (concat (_ bv0 24)
+  (select a (bvadd ax (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_
+  bv0 24) (select a (bvadd ax (_ bv2 32)))) (_ bv16 32))) (bvshl
+  (concat (_ bv0 24) (select a (bvadd ax (_ bv3 32)))) (_ bv24 32))))
+  (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))))))))))))))))))))))))))
+  (bvand (bvnot (_ bv0 1)) (bvand (bvand aa (bvand e (bvand f (bvand
+  ab (bvand g (bvand h (bvand i (bvand j k)))))))) (ite (= aw an) (_
+  bv1 1) (_ bv0 1))))))))
+(check-sat)
\ No newline at end of file
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index bb53c15b0..d65e022c9 100644
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -13,6 +13,8 @@
 # custom finder modules).
 set(CxxTest_HOME ${CXXTEST_DIR})
 find_package(CxxTest REQUIRED)
+find_package(GTest REQUIRED)
+include(GoogleTest)
 
 include_directories(.)
 include_directories(${PROJECT_SOURCE_DIR}/src)
@@ -36,9 +38,47 @@ set(CVC4_CXXTEST_FLAGS_BLACK
 set(CVC4_CXXTEST_FLAGS_WHITE -fno-access-control ${CVC4_CXXTEST_FLAGS_BLACK})
 
 # Generate and add unit test.
+macro(cvc4_add_unit_test is_white name output_dir)
+  set(test_src ${CMAKE_CURRENT_LIST_DIR}/${name}.cpp)
+  add_executable(${name} ${test_src})
+  gtest_add_tests(TARGET ${name})
+  target_link_libraries(${name} main-test)
+  target_link_libraries(${name} GTest::GTest)
+  target_link_libraries(${name} GTest::Main)
+  if(USE_LFSC)
+    # We don't link against LFSC, because CVC4 is already linked against it.
+    target_include_directories(${name} PRIVATE ${LFSC_INCLUDE_DIR})
+  endif()
+  if(USE_POLY)
+    # We don't link against libpoly, because CVC4 is already linked against it.
+    target_include_directories(${name} PRIVATE ${POLY_INCLUDE_DIR})
+  endif()
+  if(${is_white})
+    target_compile_options(${name} PRIVATE -fno-access-control)
+  endif()
+  add_dependencies(build-units ${name})
+  # Generate into bin/test/unit/<output_dir>.
+  set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/unit/${output_dir})
+  set_target_properties(${name}
+    PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir})
+  # The test target is prefixed with test identifier 'unit/' and the path,
+  # e.g., for '<output_dir>/myunittest.h'
+  #   we create test target 'unit/<output_dir>/myunittest'
+  #   and run it with 'ctest -R "example/<output_dir>/myunittest"'.
+  if("${output_dir}" STREQUAL "")
+    set(test_name unit/${name})
+  else()
+    set(test_name unit/${output_dir}/${name})
+  endif()
+  add_test(${test_name} ${test_bin_dir}/${name})
+  set_tests_properties(${test_name} PROPERTIES LABELS "unit")
+endmacro()
+
+# Generate and add unit test.
 # Note: we do not use cxxtest_add_test from the FindCxxTest module since it
 #       does not allow test names containing '/'.
-macro(cvc4_add_unit_test is_white name output_dir)
+# !! This macro will be removed when all unit tests are migrated to Google Test.
+macro(cvc4_add_cxx_unit_test is_white name output_dir)
   # generate the test sources
   set(test_src ${CMAKE_CURRENT_BINARY_DIR}/${name}.cpp)
   set(test_header ${CMAKE_CURRENT_LIST_DIR}/${name}.h)
@@ -110,6 +150,15 @@ macro(cvc4_add_unit_test_white name output_dir)
   cvc4_add_unit_test(TRUE ${name} ${output_dir})
 endmacro()
 
+# !! Will be removed when all unit tests are migrated to Google Test.
+macro(cvc4_add_cxx_unit_test_black name output_dir)
+  cvc4_add_cxx_unit_test(FALSE ${name} ${output_dir})
+endmacro()
+# !! Will be removed when all unit tests are migrated to Google Test.
+macro(cvc4_add_cxx_unit_test_white name output_dir)
+  cvc4_add_cxx_unit_test(TRUE ${name} ${output_dir})
+endmacro()
+
 add_subdirectory(api)
 add_subdirectory(base)
 add_subdirectory(context)
diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index 1412c7f66..a8c696c00 100644
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -12,10 +12,10 @@
 # Add unit tests
 
 cvc4_add_unit_test_black(datatype_api_black api)
-cvc4_add_unit_test_black(op_black api)
+cvc4_add_cxx_unit_test_black(op_black api)
 cvc4_add_unit_test_black(result_black api)
-cvc4_add_unit_test_black(solver_black api)
-cvc4_add_unit_test_black(sort_black api)
-cvc4_add_unit_test_black(term_black api)
-cvc4_add_unit_test_black(grammar_black api)
+cvc4_add_cxx_unit_test_black(solver_black api)
+cvc4_add_cxx_unit_test_black(sort_black api)
+cvc4_add_cxx_unit_test_black(term_black api)
+cvc4_add_cxx_unit_test_black(grammar_black api)
 
diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.cpp
index 4564b261a..f61637221 100644
--- a/test/unit/api/datatype_api_black.h
+++ b/test/unit/api/datatype_api_black.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file datatype_api_black.h
+/*! \file datatype_api_black.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Andrew Reynolds, Aina Niemetz, Andres Noetzli
@@ -14,39 +14,11 @@
  ** Black box testing of the datatype classes of the C++ API.
  **/
 
-#include <cxxtest/TestSuite.h>
-
-#include "api/cvc4cpp.h"
+#include "test_api.h"
 
 using namespace CVC4::api;
 
-class DatatypeBlack : public CxxTest::TestSuite
-{
- public:
-  void setUp() override;
-  void tearDown() override;
-
-  void testMkDatatypeSort();
-  void testMkDatatypeSorts();
-
-  void testDatatypeStructs();
-  void testDatatypeNames();
-
-  void testParametricDatatype();
-
-  void testDatatypeSimplyRec();
-
-  void testDatatypeSpecializedCons();
-
- private:
-  Solver d_solver;
-};
-
-void DatatypeBlack::setUp() {}
-
-void DatatypeBlack::tearDown() {}
-
-void DatatypeBlack::testMkDatatypeSort()
+TEST_F(TestApi, mkDatatypeSort)
 {
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
   DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
@@ -58,12 +30,12 @@ void DatatypeBlack::testMkDatatypeSort()
   Datatype d = listSort.getDatatype();
   DatatypeConstructor consConstr = d[0];
   DatatypeConstructor nilConstr = d[1];
-  TS_ASSERT_THROWS(d[2], CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(consConstr.getConstructorTerm());
-  TS_ASSERT_THROWS_NOTHING(nilConstr.getConstructorTerm());
+  EXPECT_THROW(d[2], CVC4ApiException);
+  ASSERT_NO_THROW(consConstr.getConstructorTerm());
+  ASSERT_NO_THROW(nilConstr.getConstructorTerm());
 }
 
-void DatatypeBlack::testMkDatatypeSorts()
+TEST_F(TestApi, mkDatatypeSorts)
 {
   /* Create two mutual datatypes corresponding to this definition
    * block:
@@ -103,33 +75,32 @@ void DatatypeBlack::testMkDatatypeSorts()
   dtdecls.push_back(tree);
   dtdecls.push_back(list);
   std::vector<Sort> dtsorts;
-  TS_ASSERT_THROWS_NOTHING(dtsorts =
-                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
-  TS_ASSERT(dtsorts.size() == dtdecls.size());
-  for (unsigned i = 0, ndecl = dtdecls.size(); i < ndecl; i++)
+  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  ASSERT_EQ(dtsorts.size(), dtdecls.size());
+  for (size_t i = 0, ndecl = dtdecls.size(); i < ndecl; i++)
   {
-    TS_ASSERT(dtsorts[i].isDatatype());
-    TS_ASSERT(!dtsorts[i].getDatatype().isFinite());
-    TS_ASSERT(dtsorts[i].getDatatype().getName() == dtdecls[i].getName());
+    ASSERT_TRUE(dtsorts[i].isDatatype());
+    EXPECT_FALSE(dtsorts[i].getDatatype().isFinite());
+    EXPECT_EQ(dtsorts[i].getDatatype().getName(), dtdecls[i].getName());
   }
   // verify the resolution was correct
   Datatype dtTree = dtsorts[0].getDatatype();
   DatatypeConstructor dtcTreeNode = dtTree[0];
-  TS_ASSERT(dtcTreeNode.getName() == "node");
+  EXPECT_EQ(dtcTreeNode.getName(), "node");
   DatatypeSelector dtsTreeNodeLeft = dtcTreeNode[0];
-  TS_ASSERT(dtsTreeNodeLeft.getName() == "left");
+  EXPECT_EQ(dtsTreeNodeLeft.getName(), "left");
   // argument type should have resolved to be recursive
-  TS_ASSERT(dtsTreeNodeLeft.getRangeSort().isDatatype());
-  TS_ASSERT(dtsTreeNodeLeft.getRangeSort() == dtsorts[0]);
+  EXPECT_TRUE(dtsTreeNodeLeft.getRangeSort().isDatatype());
+  EXPECT_EQ(dtsTreeNodeLeft.getRangeSort(), dtsorts[0]);
 
   // fails due to empty datatype
   std::vector<DatatypeDecl> dtdeclsBad;
   DatatypeDecl emptyD = d_solver.mkDatatypeDecl("emptyD");
   dtdeclsBad.push_back(emptyD);
-  TS_ASSERT_THROWS(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException&);
+  EXPECT_THROW(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException);
 }
 
-void DatatypeBlack::testDatatypeStructs()
+TEST_F(TestApi, datatypeStructs)
 {
   Sort intSort = d_solver.getIntegerSort();
   Sort boolSort = d_solver.getBooleanSort();
@@ -140,21 +111,21 @@ void DatatypeBlack::testDatatypeStructs()
   cons.addSelector("head", intSort);
   cons.addSelectorSelf("tail");
   Sort nullSort;
-  TS_ASSERT_THROWS(cons.addSelector("null", nullSort), CVC4ApiException&);
+  EXPECT_THROW(cons.addSelector("null", nullSort), CVC4ApiException);
   dtypeSpec.addConstructor(cons);
   DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   Datatype dt = dtypeSort.getDatatype();
-  TS_ASSERT(!dt.isCodatatype());
-  TS_ASSERT(!dt.isTuple());
-  TS_ASSERT(!dt.isRecord());
-  TS_ASSERT(!dt.isFinite());
-  TS_ASSERT(dt.isWellFounded());
+  EXPECT_FALSE(dt.isCodatatype());
+  EXPECT_FALSE(dt.isTuple());
+  EXPECT_FALSE(dt.isRecord());
+  EXPECT_FALSE(dt.isFinite());
+  EXPECT_TRUE(dt.isWellFounded());
   // get constructor
   DatatypeConstructor dcons = dt[0];
   Term consTerm = dcons.getConstructorTerm();
-  TS_ASSERT(dcons.getNumSelectors() == 2);
+  EXPECT_EQ(dcons.getNumSelectors(), 2);
 
   // create datatype sort to test
   DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum");
@@ -166,8 +137,8 @@ void DatatypeBlack::testDatatypeStructs()
   dtypeSpecEnum.addConstructor(cc);
   Sort dtypeSortEnum = d_solver.mkDatatypeSort(dtypeSpecEnum);
   Datatype dtEnum = dtypeSortEnum.getDatatype();
-  TS_ASSERT(!dtEnum.isTuple());
-  TS_ASSERT(dtEnum.isFinite());
+  EXPECT_FALSE(dtEnum.isTuple());
+  EXPECT_TRUE(dtEnum.isFinite());
 
   // create codatatype
   DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true);
@@ -178,39 +149,39 @@ void DatatypeBlack::testDatatypeStructs()
   dtypeSpecStream.addConstructor(consStream);
   Sort dtypeSortStream = d_solver.mkDatatypeSort(dtypeSpecStream);
   Datatype dtStream = dtypeSortStream.getDatatype();
-  TS_ASSERT(dtStream.isCodatatype());
-  TS_ASSERT(!dtStream.isFinite());
+  EXPECT_TRUE(dtStream.isCodatatype());
+  EXPECT_FALSE(dtStream.isFinite());
   // codatatypes may be well-founded
-  TS_ASSERT(dtStream.isWellFounded());
+  EXPECT_TRUE(dtStream.isWellFounded());
 
   // create tuple
   Sort tupSort = d_solver.mkTupleSort({boolSort});
   Datatype dtTuple = tupSort.getDatatype();
-  TS_ASSERT(dtTuple.isTuple());
-  TS_ASSERT(!dtTuple.isRecord());
-  TS_ASSERT(dtTuple.isFinite());
-  TS_ASSERT(dtTuple.isWellFounded());
+  EXPECT_TRUE(dtTuple.isTuple());
+  EXPECT_FALSE(dtTuple.isRecord());
+  EXPECT_TRUE(dtTuple.isFinite());
+  EXPECT_TRUE(dtTuple.isWellFounded());
 
   // create record
   std::vector<std::pair<std::string, Sort>> fields = {
       std::make_pair("b", boolSort), std::make_pair("i", intSort)};
   Sort recSort = d_solver.mkRecordSort(fields);
-  TS_ASSERT(recSort.isDatatype());
+  EXPECT_TRUE(recSort.isDatatype());
   Datatype dtRecord = recSort.getDatatype();
-  TS_ASSERT(!dtRecord.isTuple());
-  TS_ASSERT(dtRecord.isRecord());
-  TS_ASSERT(!dtRecord.isFinite());
-  TS_ASSERT(dtRecord.isWellFounded());
+  EXPECT_FALSE(dtRecord.isTuple());
+  EXPECT_TRUE(dtRecord.isRecord());
+  EXPECT_FALSE(dtRecord.isFinite());
+  EXPECT_TRUE(dtRecord.isWellFounded());
 }
 
-void DatatypeBlack::testDatatypeNames()
+TEST_F(TestApi, datatypeNames)
 {
   Sort intSort = d_solver.getIntegerSort();
 
   // create datatype sort to test
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
-  TS_ASSERT_THROWS_NOTHING(dtypeSpec.getName());
-  TS_ASSERT(dtypeSpec.getName() == std::string("list"));
+  ASSERT_NO_THROW(dtypeSpec.getName());
+  EXPECT_EQ(dtypeSpec.getName(), std::string("list"));
   DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", intSort);
   cons.addSelectorSelf("tail");
@@ -219,28 +190,28 @@ void DatatypeBlack::testDatatypeNames()
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   Datatype dt = dtypeSort.getDatatype();
-  TS_ASSERT(dt.getName() == std::string("list"));
-  TS_ASSERT_THROWS_NOTHING(dt.getConstructor("nil"));
-  TS_ASSERT_THROWS_NOTHING(dt["cons"]);
-  TS_ASSERT_THROWS(dt.getConstructor("head"), CVC4ApiException&);
-  TS_ASSERT_THROWS(dt.getConstructor(""), CVC4ApiException&);
+  EXPECT_EQ(dt.getName(), std::string("list"));
+  ASSERT_NO_THROW(dt.getConstructor("nil"));
+  ASSERT_NO_THROW(dt["cons"]);
+  ASSERT_THROW(dt.getConstructor("head"), CVC4ApiException);
+  ASSERT_THROW(dt.getConstructor(""), CVC4ApiException);
 
   DatatypeConstructor dcons = dt[0];
-  TS_ASSERT(dcons.getName() == std::string("cons"));
-  TS_ASSERT_THROWS_NOTHING(dcons.getSelector("head"));
-  TS_ASSERT_THROWS_NOTHING(dcons["tail"]);
-  TS_ASSERT_THROWS(dcons.getSelector("cons"), CVC4ApiException&);
+  EXPECT_EQ(dcons.getName(), std::string("cons"));
+  ASSERT_NO_THROW(dcons.getSelector("head"));
+  ASSERT_NO_THROW(dcons["tail"]);
+  ASSERT_THROW(dcons.getSelector("cons"), CVC4ApiException);
 
   // get selector
   DatatypeSelector dselTail = dcons[1];
-  TS_ASSERT(dselTail.getName() == std::string("tail"));
-  TS_ASSERT(dselTail.getRangeSort() == dtypeSort);
+  EXPECT_EQ(dselTail.getName(), std::string("tail"));
+  EXPECT_EQ(dselTail.getRangeSort(), dtypeSort);
 
   // possible to construct null datatype declarations if not using solver
-  TS_ASSERT_THROWS(DatatypeDecl().getName(), CVC4ApiException&);
+  ASSERT_THROW(DatatypeDecl().getName(), CVC4ApiException);
 }
 
-void DatatypeBlack::testParametricDatatype()
+TEST_F(TestApi, parametricDatatype)
 {
   std::vector<Sort> v;
   Sort t1 = d_solver.mkParamSort("T1");
@@ -257,7 +228,7 @@ void DatatypeBlack::testParametricDatatype()
 
   Sort pairType = d_solver.mkDatatypeSort(pairSpec);
 
-  TS_ASSERT(pairType.getDatatype().isParametric());
+  EXPECT_TRUE(pairType.getDatatype().isParametric());
 
   v.clear();
   v.push_back(d_solver.getIntegerSort());
@@ -276,49 +247,49 @@ void DatatypeBlack::testParametricDatatype()
   v.push_back(d_solver.getRealSort());
   Sort pairIntReal = pairType.instantiate(v);
 
-  TS_ASSERT_DIFFERS(pairIntInt, pairRealReal);
-  TS_ASSERT_DIFFERS(pairIntReal, pairRealReal);
-  TS_ASSERT_DIFFERS(pairRealInt, pairRealReal);
-  TS_ASSERT_DIFFERS(pairIntInt, pairIntReal);
-  TS_ASSERT_DIFFERS(pairIntInt, pairRealInt);
-  TS_ASSERT_DIFFERS(pairIntReal, pairRealInt);
-
-  TS_ASSERT(pairRealReal.isComparableTo(pairRealReal));
-  TS_ASSERT(!pairIntReal.isComparableTo(pairRealReal));
-  TS_ASSERT(!pairRealInt.isComparableTo(pairRealReal));
-  TS_ASSERT(!pairIntInt.isComparableTo(pairRealReal));
-  TS_ASSERT(!pairRealReal.isComparableTo(pairRealInt));
-  TS_ASSERT(!pairIntReal.isComparableTo(pairRealInt));
-  TS_ASSERT(pairRealInt.isComparableTo(pairRealInt));
-  TS_ASSERT(!pairIntInt.isComparableTo(pairRealInt));
-  TS_ASSERT(!pairRealReal.isComparableTo(pairIntReal));
-  TS_ASSERT(pairIntReal.isComparableTo(pairIntReal));
-  TS_ASSERT(!pairRealInt.isComparableTo(pairIntReal));
-  TS_ASSERT(!pairIntInt.isComparableTo(pairIntReal));
-  TS_ASSERT(!pairRealReal.isComparableTo(pairIntInt));
-  TS_ASSERT(!pairIntReal.isComparableTo(pairIntInt));
-  TS_ASSERT(!pairRealInt.isComparableTo(pairIntInt));
-  TS_ASSERT(pairIntInt.isComparableTo(pairIntInt));
-
-  TS_ASSERT(pairRealReal.isSubsortOf(pairRealReal));
-  TS_ASSERT(!pairIntReal.isSubsortOf(pairRealReal));
-  TS_ASSERT(!pairRealInt.isSubsortOf(pairRealReal));
-  TS_ASSERT(!pairIntInt.isSubsortOf(pairRealReal));
-  TS_ASSERT(!pairRealReal.isSubsortOf(pairRealInt));
-  TS_ASSERT(!pairIntReal.isSubsortOf(pairRealInt));
-  TS_ASSERT(pairRealInt.isSubsortOf(pairRealInt));
-  TS_ASSERT(!pairIntInt.isSubsortOf(pairRealInt));
-  TS_ASSERT(!pairRealReal.isSubsortOf(pairIntReal));
-  TS_ASSERT(pairIntReal.isSubsortOf(pairIntReal));
-  TS_ASSERT(!pairRealInt.isSubsortOf(pairIntReal));
-  TS_ASSERT(!pairIntInt.isSubsortOf(pairIntReal));
-  TS_ASSERT(!pairRealReal.isSubsortOf(pairIntInt));
-  TS_ASSERT(!pairIntReal.isSubsortOf(pairIntInt));
-  TS_ASSERT(!pairRealInt.isSubsortOf(pairIntInt));
-  TS_ASSERT(pairIntInt.isSubsortOf(pairIntInt));
+  EXPECT_NE(pairIntInt, pairRealReal);
+  EXPECT_NE(pairIntReal, pairRealReal);
+  EXPECT_NE(pairRealInt, pairRealReal);
+  EXPECT_NE(pairIntInt, pairIntReal);
+  EXPECT_NE(pairIntInt, pairRealInt);
+  EXPECT_NE(pairIntReal, pairRealInt);
+
+  EXPECT_TRUE(pairRealReal.isComparableTo(pairRealReal));
+  EXPECT_FALSE(pairIntReal.isComparableTo(pairRealReal));
+  EXPECT_FALSE(pairRealInt.isComparableTo(pairRealReal));
+  EXPECT_FALSE(pairIntInt.isComparableTo(pairRealReal));
+  EXPECT_FALSE(pairRealReal.isComparableTo(pairRealInt));
+  EXPECT_FALSE(pairIntReal.isComparableTo(pairRealInt));
+  EXPECT_TRUE(pairRealInt.isComparableTo(pairRealInt));
+  EXPECT_FALSE(pairIntInt.isComparableTo(pairRealInt));
+  EXPECT_FALSE(pairRealReal.isComparableTo(pairIntReal));
+  EXPECT_TRUE(pairIntReal.isComparableTo(pairIntReal));
+  EXPECT_FALSE(pairRealInt.isComparableTo(pairIntReal));
+  EXPECT_FALSE(pairIntInt.isComparableTo(pairIntReal));
+  EXPECT_FALSE(pairRealReal.isComparableTo(pairIntInt));
+  EXPECT_FALSE(pairIntReal.isComparableTo(pairIntInt));
+  EXPECT_FALSE(pairRealInt.isComparableTo(pairIntInt));
+  EXPECT_TRUE(pairIntInt.isComparableTo(pairIntInt));
+
+  EXPECT_TRUE(pairRealReal.isSubsortOf(pairRealReal));
+  EXPECT_FALSE(pairIntReal.isSubsortOf(pairRealReal));
+  EXPECT_FALSE(pairRealInt.isSubsortOf(pairRealReal));
+  EXPECT_FALSE(pairIntInt.isSubsortOf(pairRealReal));
+  EXPECT_FALSE(pairRealReal.isSubsortOf(pairRealInt));
+  EXPECT_FALSE(pairIntReal.isSubsortOf(pairRealInt));
+  EXPECT_TRUE(pairRealInt.isSubsortOf(pairRealInt));
+  EXPECT_FALSE(pairIntInt.isSubsortOf(pairRealInt));
+  EXPECT_FALSE(pairRealReal.isSubsortOf(pairIntReal));
+  EXPECT_TRUE(pairIntReal.isSubsortOf(pairIntReal));
+  EXPECT_FALSE(pairRealInt.isSubsortOf(pairIntReal));
+  EXPECT_FALSE(pairIntInt.isSubsortOf(pairIntReal));
+  EXPECT_FALSE(pairRealReal.isSubsortOf(pairIntInt));
+  EXPECT_FALSE(pairIntReal.isSubsortOf(pairIntInt));
+  EXPECT_FALSE(pairRealInt.isSubsortOf(pairIntInt));
+  EXPECT_TRUE(pairIntInt.isSubsortOf(pairIntInt));
 }
 
-void DatatypeBlack::testDatatypeSimplyRec()
+TEST_F(TestApi, datatypeSimplyRec)
 {
   /* Create mutual datatypes corresponding to this definition block:
    *
@@ -365,15 +336,14 @@ void DatatypeBlack::testDatatypeSimplyRec()
   dtdecls.push_back(ns);
   // this is well-founded and has no nested recursion
   std::vector<Sort> dtsorts;
-  TS_ASSERT_THROWS_NOTHING(dtsorts =
-                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
-  TS_ASSERT(dtsorts.size() == 3);
-  TS_ASSERT(dtsorts[0].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[1].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[2].getDatatype().isWellFounded());
-  TS_ASSERT(!dtsorts[0].getDatatype().hasNestedRecursion());
-  TS_ASSERT(!dtsorts[1].getDatatype().hasNestedRecursion());
-  TS_ASSERT(!dtsorts[2].getDatatype().hasNestedRecursion());
+  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  ASSERT_EQ(dtsorts.size(), 3);
+  EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[2].getDatatype().isWellFounded());
+  EXPECT_FALSE(dtsorts[0].getDatatype().hasNestedRecursion());
+  EXPECT_FALSE(dtsorts[1].getDatatype().hasNestedRecursion());
+  EXPECT_FALSE(dtsorts[2].getDatatype().hasNestedRecursion());
 
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -397,14 +367,13 @@ void DatatypeBlack::testDatatypeSimplyRec()
 
   dtsorts.clear();
   // this is not well-founded due to non-simple recursion
-  TS_ASSERT_THROWS_NOTHING(dtsorts =
-                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
-  TS_ASSERT(dtsorts.size() == 1);
-  TS_ASSERT(dtsorts[0].getDatatype()[0][0].getRangeSort().isArray());
-  TS_ASSERT(dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort()
-            == dtsorts[0]);
-  TS_ASSERT(dtsorts[0].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion());
+  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  ASSERT_EQ(dtsorts.size(), 1);
+  ASSERT_TRUE(dtsorts[0].getDatatype()[0][0].getRangeSort().isArray());
+  EXPECT_EQ(dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort(),
+            dtsorts[0]);
+  EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
 
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -437,13 +406,12 @@ void DatatypeBlack::testDatatypeSimplyRec()
 
   dtsorts.clear();
   // both are well-founded and have nested recursion
-  TS_ASSERT_THROWS_NOTHING(dtsorts =
-                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
-  TS_ASSERT(dtsorts.size() == 2);
-  TS_ASSERT(dtsorts[0].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[1].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion());
-  TS_ASSERT(dtsorts[1].getDatatype().hasNestedRecursion());
+  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  ASSERT_EQ(dtsorts.size(), 2);
+  EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
+  EXPECT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion());
 
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -476,13 +444,12 @@ void DatatypeBlack::testDatatypeSimplyRec()
 
   dtsorts.clear();
   // both are well-founded and have nested recursion
-  TS_ASSERT_THROWS_NOTHING(dtsorts =
-                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
-  TS_ASSERT(dtsorts.size() == 2);
-  TS_ASSERT(dtsorts[0].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[1].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion());
-  TS_ASSERT(dtsorts[1].getDatatype().hasNestedRecursion());
+  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  ASSERT_EQ(dtsorts.size(), 2);
+  EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
+  EXPECT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion());
 
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -515,14 +482,13 @@ void DatatypeBlack::testDatatypeSimplyRec()
   dtdecls.push_back(list5);
 
   // well-founded and has nested recursion
-  TS_ASSERT_THROWS_NOTHING(dtsorts =
-                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
-  TS_ASSERT(dtsorts.size() == 1);
-  TS_ASSERT(dtsorts[0].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion());
+  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  ASSERT_EQ(dtsorts.size(), 1);
+  EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
 }
 
-void DatatypeBlack::testDatatypeSpecializedCons()
+TEST_F(TestApi, datatypeSpecializedCons)
 {
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -555,9 +521,8 @@ void DatatypeBlack::testDatatypeSpecializedCons()
 
   std::vector<Sort> dtsorts;
   // make the datatype sorts
-  TS_ASSERT_THROWS_NOTHING(dtsorts =
-                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
-  TS_ASSERT(dtsorts.size() == 1);
+  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  ASSERT_EQ(dtsorts.size(), 1);
   Datatype d = dtsorts[0].getDatatype();
   DatatypeConstructor nilc = d[0];
 
@@ -568,9 +533,8 @@ void DatatypeBlack::testDatatypeSpecializedCons()
 
   Term testConsTerm;
   // get the specialized constructor term for list[Int]
-  TS_ASSERT_THROWS_NOTHING(testConsTerm =
-                               nilc.getSpecializedConstructorTerm(listInt));
-  TS_ASSERT(testConsTerm != nilc.getConstructorTerm());
+  ASSERT_NO_THROW(testConsTerm = nilc.getSpecializedConstructorTerm(listInt));
+  EXPECT_NE(testConsTerm, nilc.getConstructorTerm());
   // error to get the specialized constructor term for Int
-  TS_ASSERT_THROWS(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException&);
+  EXPECT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException);
 }
diff --git a/test/unit/api/result_black.cpp b/test/unit/api/result_black.cpp
new file mode 100644
index 000000000..260845495
--- /dev/null
+++ b/test/unit/api/result_black.cpp
@@ -0,0 +1,115 @@
+/*********************                                                        */
+/*! \file result_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of the Result class
+ **/
+
+#include "test_api.h"
+
+using namespace CVC4::api;
+
+class TestApiResultBlack : public TestApi
+{
+};
+
+TEST_F(TestApiResultBlack, isNull)
+{
+  Result res_null;
+  ASSERT_TRUE(res_null.isNull());
+  ASSERT_FALSE(res_null.isSat());
+  ASSERT_FALSE(res_null.isUnsat());
+  ASSERT_FALSE(res_null.isSatUnknown());
+  ASSERT_FALSE(res_null.isEntailed());
+  ASSERT_FALSE(res_null.isNotEntailed());
+  ASSERT_FALSE(res_null.isEntailmentUnknown());
+  Sort u_sort = d_solver.mkUninterpretedSort("u");
+  Term x = d_solver.mkVar(u_sort, "x");
+  d_solver.assertFormula(x.eqTerm(x));
+  Result res = d_solver.checkSat();
+  ASSERT_FALSE(res.isNull());
+}
+
+TEST_F(TestApiResultBlack, eq)
+{
+  Sort u_sort = d_solver.mkUninterpretedSort("u");
+  Term x = d_solver.mkVar(u_sort, "x");
+  d_solver.assertFormula(x.eqTerm(x));
+  Result res;
+  Result res2 = d_solver.checkSat();
+  Result res3 = d_solver.checkSat();
+  res = res2;
+  EXPECT_EQ(res, res2);
+  EXPECT_EQ(res3, res2);
+}
+
+TEST_F(TestApiResultBlack, isSat)
+{
+  Sort u_sort = d_solver.mkUninterpretedSort("u");
+  Term x = d_solver.mkVar(u_sort, "x");
+  d_solver.assertFormula(x.eqTerm(x));
+  Result res = d_solver.checkSat();
+  ASSERT_TRUE(res.isSat());
+  ASSERT_FALSE(res.isSatUnknown());
+}
+
+TEST_F(TestApiResultBlack, isUnsat)
+{
+  Sort u_sort = d_solver.mkUninterpretedSort("u");
+  Term x = d_solver.mkVar(u_sort, "x");
+  d_solver.assertFormula(x.eqTerm(x).notTerm());
+  Result res = d_solver.checkSat();
+  ASSERT_TRUE(res.isUnsat());
+  ASSERT_FALSE(res.isSatUnknown());
+}
+
+TEST_F(TestApiResultBlack, isSatUnknown)
+{
+  d_solver.setLogic("QF_NIA");
+  d_solver.setOption("incremental", "false");
+  d_solver.setOption("solve-int-as-bv", "32");
+  Sort int_sort = d_solver.getIntegerSort();
+  Term x = d_solver.mkVar(int_sort, "x");
+  d_solver.assertFormula(x.eqTerm(x).notTerm());
+  Result res = d_solver.checkSat();
+  ASSERT_FALSE(res.isSat());
+  ASSERT_TRUE(res.isSatUnknown());
+}
+
+TEST_F(TestApiResultBlack, isEntailed)
+{
+  d_solver.setOption("incremental", "true");
+  Sort u_sort = d_solver.mkUninterpretedSort("u");
+  Term x = d_solver.mkConst(u_sort, "x");
+  Term y = d_solver.mkConst(u_sort, "y");
+  Term a = x.eqTerm(y).notTerm();
+  Term b = x.eqTerm(y);
+  d_solver.assertFormula(a);
+  Result entailed = d_solver.checkEntailed(a);
+  ASSERT_TRUE(entailed.isEntailed());
+  ASSERT_FALSE(entailed.isEntailmentUnknown());
+  Result not_entailed = d_solver.checkEntailed(b);
+  ASSERT_TRUE(not_entailed.isNotEntailed());
+  ASSERT_FALSE(not_entailed.isEntailmentUnknown());
+}
+
+TEST_F(TestApiResultBlack, isEntailmentUnknown)
+{
+  d_solver.setLogic("QF_NIA");
+  d_solver.setOption("incremental", "false");
+  d_solver.setOption("solve-int-as-bv", "32");
+  Sort int_sort = d_solver.getIntegerSort();
+  Term x = d_solver.mkVar(int_sort, "x");
+  d_solver.assertFormula(x.eqTerm(x).notTerm());
+  Result res = d_solver.checkEntailed(x.eqTerm(x));
+  ASSERT_FALSE(res.isEntailed());
+  ASSERT_TRUE(res.isEntailmentUnknown());
+  EXPECT_EQ(res.getUnknownExplanation(), "UNKNOWN_REASON");
+}
diff --git a/test/unit/api/result_black.h b/test/unit/api/result_black.h
deleted file mode 100644
index aaa59e506..000000000
--- a/test/unit/api/result_black.h
+++ /dev/null
@@ -1,132 +0,0 @@
-/*********************                                                        */
-/*! \file result_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of the Result class
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "api/cvc4cpp.h"
-
-using namespace CVC4::api;
-
-class ResultBlack : public CxxTest::TestSuite
-{
- public:
-  void setUp() { d_solver.reset(new Solver()); }
-  void tearDown() override { d_solver.reset(nullptr); }
-
-  void testIsNull();
-  void testEq();
-  void testIsSat();
-  void testIsUnsat();
-  void testIsSatUnknown();
-  void testIsEntailed();
-  void testIsEntailmentUnknown();
-
- private:
-  std::unique_ptr<Solver> d_solver;
-};
-
-void ResultBlack::testIsNull()
-{
-  Result res_null;
-  TS_ASSERT(res_null.isNull());
-  TS_ASSERT(!res_null.isSat());
-  TS_ASSERT(!res_null.isUnsat());
-  TS_ASSERT(!res_null.isSatUnknown());
-  TS_ASSERT(!res_null.isEntailed());
-  TS_ASSERT(!res_null.isNotEntailed());
-  TS_ASSERT(!res_null.isEntailmentUnknown());
-  Sort u_sort = d_solver->mkUninterpretedSort("u");
-  Term x = d_solver->mkVar(u_sort, "x");
-  d_solver->assertFormula(x.eqTerm(x));
-  Result res = d_solver->checkSat();
-  TS_ASSERT(!res.isNull());
-}
-
-void ResultBlack::testEq()
-{
-  Sort u_sort = d_solver->mkUninterpretedSort("u");
-  Term x = d_solver->mkVar(u_sort, "x");
-  d_solver->assertFormula(x.eqTerm(x));
-  Result res;
-  Result res2 = d_solver->checkSat();
-  Result res3 = d_solver->checkSat();
-  res = res2;
-  TS_ASSERT_EQUALS(res, res2);
-  TS_ASSERT_EQUALS(res3, res2);
-}
-
-void ResultBlack::testIsSat()
-{
-  Sort u_sort = d_solver->mkUninterpretedSort("u");
-  Term x = d_solver->mkVar(u_sort, "x");
-  d_solver->assertFormula(x.eqTerm(x));
-  Result res = d_solver->checkSat();
-  TS_ASSERT(res.isSat());
-  TS_ASSERT(!res.isSatUnknown());
-}
-
-void ResultBlack::testIsUnsat()
-{
-  Sort u_sort = d_solver->mkUninterpretedSort("u");
-  Term x = d_solver->mkVar(u_sort, "x");
-  d_solver->assertFormula(x.eqTerm(x).notTerm());
-  Result res = d_solver->checkSat();
-  TS_ASSERT(res.isUnsat());
-  TS_ASSERT(!res.isSatUnknown());
-}
-
-void ResultBlack::testIsSatUnknown()
-{
-  d_solver->setLogic("QF_NIA");
-  d_solver->setOption("incremental", "false");
-  d_solver->setOption("solve-int-as-bv", "32");
-  Sort int_sort = d_solver->getIntegerSort();
-  Term x = d_solver->mkVar(int_sort, "x");
-  d_solver->assertFormula(x.eqTerm(x).notTerm());
-  Result res = d_solver->checkSat();
-  TS_ASSERT(!res.isSat());
-  TS_ASSERT(res.isSatUnknown());
-}
-
-void ResultBlack::testIsEntailed()
-{
-  d_solver->setOption("incremental", "true");
-  Sort u_sort = d_solver->mkUninterpretedSort("u");
-  Term x = d_solver->mkConst(u_sort, "x");
-  Term y = d_solver->mkConst(u_sort, "y");
-  Term a = x.eqTerm(y).notTerm();
-  Term b = x.eqTerm(y);
-  d_solver->assertFormula(a);
-  Result entailed = d_solver->checkEntailed(a);
-  TS_ASSERT(entailed.isEntailed());
-  TS_ASSERT(!entailed.isEntailmentUnknown());
-  Result not_entailed = d_solver->checkEntailed(b);
-  TS_ASSERT(not_entailed.isNotEntailed());
-  TS_ASSERT(!not_entailed.isEntailmentUnknown());
-}
-
-void ResultBlack::testIsEntailmentUnknown()
-{
-  d_solver->setLogic("QF_NIA");
-  d_solver->setOption("incremental", "false");
-  d_solver->setOption("solve-int-as-bv", "32");
-  Sort int_sort = d_solver->getIntegerSort();
-  Term x = d_solver->mkVar(int_sort, "x");
-  d_solver->assertFormula(x.eqTerm(x).notTerm());
-  Result res = d_solver->checkEntailed(x.eqTerm(x));
-  TS_ASSERT(!res.isEntailed());
-  TS_ASSERT(res.isEntailmentUnknown());
-  TS_ASSERT_EQUALS(res.getUnknownExplanation(), "UNKNOWN_REASON");
-}
-
diff --git a/test/unit/base/CMakeLists.txt b/test/unit/base/CMakeLists.txt
index 81d27c040..8274a5a46 100644
--- a/test/unit/base/CMakeLists.txt
+++ b/test/unit/base/CMakeLists.txt
@@ -11,4 +11,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(map_util_black base)
+cvc4_add_cxx_unit_test_black(map_util_black base)
diff --git a/test/unit/context/CMakeLists.txt b/test/unit/context/CMakeLists.txt
index 6752f0e78..51465c622 100644
--- a/test/unit/context/CMakeLists.txt
+++ b/test/unit/context/CMakeLists.txt
@@ -11,10 +11,10 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(cdlist_black context)
-cvc4_add_unit_test_black(cdmap_black context)
-cvc4_add_unit_test_white(cdmap_white context)
-cvc4_add_unit_test_black(cdo_black context)
-cvc4_add_unit_test_black(context_black context)
-cvc4_add_unit_test_black(context_mm_black context)
-cvc4_add_unit_test_white(context_white context)
+cvc4_add_cxx_unit_test_black(cdlist_black context)
+cvc4_add_cxx_unit_test_black(cdmap_black context)
+cvc4_add_cxx_unit_test_white(cdmap_white context)
+cvc4_add_cxx_unit_test_black(cdo_black context)
+cvc4_add_cxx_unit_test_black(context_black context)
+cvc4_add_cxx_unit_test_black(context_mm_black context)
+cvc4_add_cxx_unit_test_white(context_white context)
diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt
index c10648c03..6c0abc4ab 100644
--- a/test/unit/expr/CMakeLists.txt
+++ b/test/unit/expr/CMakeLists.txt
@@ -11,20 +11,20 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(attribute_black expr)
-cvc4_add_unit_test_white(attribute_white expr)
-cvc4_add_unit_test_black(expr_manager_public expr)
-cvc4_add_unit_test_black(expr_public expr)
-cvc4_add_unit_test_black(kind_black expr)
-cvc4_add_unit_test_black(kind_map_black expr)
-cvc4_add_unit_test_black(node_black expr)
-cvc4_add_unit_test_black(node_algorithm_black expr)
-cvc4_add_unit_test_black(node_builder_black expr)
-cvc4_add_unit_test_black(node_manager_black expr)
-cvc4_add_unit_test_white(node_manager_white expr)
-cvc4_add_unit_test_black(node_self_iterator_black expr)
-cvc4_add_unit_test_black(node_traversal_black expr)
-cvc4_add_unit_test_white(node_white expr)
-cvc4_add_unit_test_black(symbol_table_black expr)
-cvc4_add_unit_test_black(type_cardinality_public expr)
-cvc4_add_unit_test_white(type_node_white expr)
+cvc4_add_cxx_unit_test_black(attribute_black expr)
+cvc4_add_cxx_unit_test_white(attribute_white expr)
+cvc4_add_cxx_unit_test_black(expr_manager_public expr)
+cvc4_add_cxx_unit_test_black(expr_public expr)
+cvc4_add_cxx_unit_test_black(kind_black expr)
+cvc4_add_cxx_unit_test_black(kind_map_black expr)
+cvc4_add_cxx_unit_test_black(node_black expr)
+cvc4_add_cxx_unit_test_black(node_algorithm_black expr)
+cvc4_add_cxx_unit_test_black(node_builder_black expr)
+cvc4_add_cxx_unit_test_black(node_manager_black expr)
+cvc4_add_cxx_unit_test_white(node_manager_white expr)
+cvc4_add_cxx_unit_test_black(node_self_iterator_black expr)
+cvc4_add_cxx_unit_test_black(node_traversal_black expr)
+cvc4_add_cxx_unit_test_white(node_white expr)
+cvc4_add_cxx_unit_test_black(symbol_table_black expr)
+cvc4_add_cxx_unit_test_black(type_cardinality_public expr)
+cvc4_add_cxx_unit_test_white(type_node_white expr)
diff --git a/test/unit/main/CMakeLists.txt b/test/unit/main/CMakeLists.txt
index 55307db95..59c197f04 100644
--- a/test/unit/main/CMakeLists.txt
+++ b/test/unit/main/CMakeLists.txt
@@ -11,4 +11,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(interactive_shell_black main)
+cvc4_add_cxx_unit_test_black(interactive_shell_black main)
diff --git a/test/unit/parser/CMakeLists.txt b/test/unit/parser/CMakeLists.txt
index 1bdcbd5f5..4202ea0c9 100644
--- a/test/unit/parser/CMakeLists.txt
+++ b/test/unit/parser/CMakeLists.txt
@@ -11,5 +11,5 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(parser_black parser)
-cvc4_add_unit_test_black(parser_builder_black parser)
+cvc4_add_cxx_unit_test_black(parser_black parser)
+cvc4_add_cxx_unit_test_black(parser_builder_black parser)
diff --git a/test/unit/preprocessing/CMakeLists.txt b/test/unit/preprocessing/CMakeLists.txt
index 7e142f404..a2381ba90 100644
--- a/test/unit/preprocessing/CMakeLists.txt
+++ b/test/unit/preprocessing/CMakeLists.txt
@@ -11,4 +11,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_white(pass_bv_gauss_white preprocessing)
+cvc4_add_cxx_unit_test_white(pass_bv_gauss_white preprocessing)
diff --git a/test/unit/printer/CMakeLists.txt b/test/unit/printer/CMakeLists.txt
index 3b040d1fc..93c241af9 100644
--- a/test/unit/printer/CMakeLists.txt
+++ b/test/unit/printer/CMakeLists.txt
@@ -11,4 +11,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(smt2_printer_black printer)
+cvc4_add_cxx_unit_test_black(smt2_printer_black printer)
diff --git a/test/unit/prop/CMakeLists.txt b/test/unit/prop/CMakeLists.txt
index bed0575c6..f866e5ffa 100644
--- a/test/unit/prop/CMakeLists.txt
+++ b/test/unit/prop/CMakeLists.txt
@@ -11,4 +11,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_white(cnf_stream_white prop)
+cvc4_add_cxx_unit_test_white(cnf_stream_white prop)
diff --git a/test/unit/test_api.h b/test/unit/test_api.h
new file mode 100644
index 000000000..72d0658a7
--- /dev/null
+++ b/test/unit/test_api.h
@@ -0,0 +1,27 @@
+/*********************                                                        */
+/*! \file datatype_api_black.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Common header for API unit test.
+ **/
+
+#ifndef CVC4__TEST__UNIT__TEST_API_H
+#define CVC4__TEST__UNIT__TEST_API_H
+
+#include "api/cvc4cpp.h"
+#include "gtest/gtest.h"
+
+class TestApi : public ::testing::Test
+{
+ protected:
+  CVC4::api::Solver d_solver;
+};
+
+#endif
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index 8cfd43989..334ded2d1 100644
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -8,23 +8,24 @@
 ## All rights reserved.  See the file COPYING in the top-level source
 ## directory for licensing information.
 ##
-cvc4_add_unit_test_black(regexp_operation_black theory)
-cvc4_add_unit_test_black(theory_black theory)
-cvc4_add_unit_test_white(evaluator_white theory)
-cvc4_add_unit_test_white(logic_info_white theory)
-cvc4_add_unit_test_white(sequences_rewriter_white theory)
-cvc4_add_unit_test_white(theory_arith_white theory)
-cvc4_add_unit_test_white(theory_bags_normal_form_white theory)
-cvc4_add_unit_test_white(theory_bags_rewriter_white theory)
-cvc4_add_unit_test_white(theory_bags_type_rules_white theory)
-cvc4_add_unit_test_white(theory_bv_rewriter_white theory)
-cvc4_add_unit_test_white(theory_bv_white theory)
-cvc4_add_unit_test_white(theory_engine_white theory)
-cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory)
-cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white theory)
-cvc4_add_unit_test_white(theory_sets_type_enumerator_white theory)
-cvc4_add_unit_test_white(theory_sets_type_rules_white theory)
-cvc4_add_unit_test_white(theory_strings_skolem_cache_black theory)
-cvc4_add_unit_test_white(theory_strings_word_white theory)
-cvc4_add_unit_test_white(theory_white theory)
-cvc4_add_unit_test_white(type_enumerator_white theory)
+cvc4_add_cxx_unit_test_black(regexp_operation_black theory)
+cvc4_add_cxx_unit_test_black(theory_black theory)
+cvc4_add_cxx_unit_test_white(evaluator_white theory)
+cvc4_add_cxx_unit_test_white(logic_info_white theory)
+cvc4_add_cxx_unit_test_white(sequences_rewriter_white theory)
+cvc4_add_cxx_unit_test_white(strings_rewriter_white theory)
+cvc4_add_cxx_unit_test_white(theory_arith_white theory)
+cvc4_add_cxx_unit_test_white(theory_bags_normal_form_white theory)
+cvc4_add_cxx_unit_test_white(theory_bags_rewriter_white theory)
+cvc4_add_cxx_unit_test_white(theory_bags_type_rules_white theory)
+cvc4_add_cxx_unit_test_white(theory_bv_rewriter_white theory)
+cvc4_add_cxx_unit_test_white(theory_bv_white theory)
+cvc4_add_cxx_unit_test_white(theory_engine_white theory)
+cvc4_add_cxx_unit_test_white(theory_quantifiers_bv_instantiator_white theory)
+cvc4_add_cxx_unit_test_white(theory_quantifiers_bv_inverter_white theory)
+cvc4_add_cxx_unit_test_white(theory_sets_type_enumerator_white theory)
+cvc4_add_cxx_unit_test_white(theory_sets_type_rules_white theory)
+cvc4_add_cxx_unit_test_white(theory_strings_skolem_cache_black theory)
+cvc4_add_cxx_unit_test_white(theory_strings_word_white theory)
+cvc4_add_cxx_unit_test_white(theory_white theory)
+cvc4_add_cxx_unit_test_white(type_enumerator_white theory)
diff --git a/test/unit/theory/strings_rewriter_white.h b/test/unit/theory/strings_rewriter_white.h
new file mode 100644
index 000000000..f5c7cced8
--- /dev/null
+++ b/test/unit/theory/strings_rewriter_white.h
@@ -0,0 +1,89 @@
+/*********************                                                        */
+/*! \file strings_rewriter_white.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Unit tests for the strings rewriter
+ **
+ ** Unit tests for the strings rewriter.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <memory>
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "theory/rewriter.h"
+#include "theory/strings/strings_rewriter.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::smt;
+using namespace CVC4::theory;
+using namespace CVC4::theory::strings;
+
+class StringsRewriterWhite : public CxxTest::TestSuite
+{
+ public:
+  StringsRewriterWhite() {}
+
+  void setUp() override
+  {
+    Options opts;
+    opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
+    d_em = new ExprManager;
+    d_nm = NodeManager::fromExprManager(d_em);
+    d_smt = new SmtEngine(d_nm, &opts);
+    d_scope = new SmtScope(d_smt);
+    d_smt->finishInit();
+  }
+
+  void tearDown() override
+  {
+    delete d_scope;
+    delete d_smt;
+    delete d_em;
+  }
+
+  void testRewriteLeq()
+  {
+    TypeNode intType = d_nm->integerType();
+    TypeNode strType = d_nm->stringType();
+
+    Node a = d_nm->mkConst(::CVC4::String("A"));
+    Node bc = d_nm->mkConst(::CVC4::String("BC"));
+    Node x = d_nm->mkVar("x", strType);
+    Node y = d_nm->mkVar("y", strType);
+
+    Node ax = d_nm->mkNode(STRING_CONCAT, a, x);
+    Node bcy = d_nm->mkNode(STRING_CONCAT, bc, y);
+
+    {
+      Node leq = d_nm->mkNode(STRING_LEQ, ax, bcy);
+      TS_ASSERT_EQUALS(Rewriter::rewrite(leq), d_nm->mkConst(true));
+    }
+
+    {
+      Node leq = d_nm->mkNode(STRING_LEQ, bcy, ax);
+      TS_ASSERT_EQUALS(Rewriter::rewrite(leq), d_nm->mkConst(false));
+    }
+  }
+
+ private:
+  ExprManager* d_em;
+  SmtEngine* d_smt;
+  SmtScope* d_scope;
+
+  NodeManager* d_nm;
+};
diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index 0fd7894fe..148ae9910 100644
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -11,25 +11,25 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_white(array_store_all_white util)
-cvc4_add_unit_test_white(assert_white util)
-cvc4_add_unit_test_black(binary_heap_black util)
-cvc4_add_unit_test_black(bitvector_black util)
-cvc4_add_unit_test_black(boolean_simplification_black util)
-cvc4_add_unit_test_black(cardinality_public util)
-cvc4_add_unit_test_white(check_white util)
-cvc4_add_unit_test_black(configuration_black util)
-cvc4_add_unit_test_black(datatype_black util)
-cvc4_add_unit_test_black(exception_black util)
+cvc4_add_cxx_unit_test_white(array_store_all_white util)
+cvc4_add_cxx_unit_test_white(assert_white util)
+cvc4_add_cxx_unit_test_black(binary_heap_black util)
+cvc4_add_cxx_unit_test_black(bitvector_black util)
+cvc4_add_cxx_unit_test_black(boolean_simplification_black util)
+cvc4_add_cxx_unit_test_black(cardinality_public util)
+cvc4_add_cxx_unit_test_white(check_white util)
+cvc4_add_cxx_unit_test_black(configuration_black util)
+cvc4_add_cxx_unit_test_black(datatype_black util)
+cvc4_add_cxx_unit_test_black(exception_black util)
 if(CVC4_USE_SYMFPU)
-cvc4_add_unit_test_black(floatingpoint_black util)
+cvc4_add_cxx_unit_test_black(floatingpoint_black util)
 endif()
-cvc4_add_unit_test_black(integer_black util)
-cvc4_add_unit_test_white(integer_white util)
-cvc4_add_unit_test_black(output_black util)
-cvc4_add_unit_test_black(rational_black util)
-cvc4_add_unit_test_white(rational_white util)
+cvc4_add_cxx_unit_test_black(integer_black util)
+cvc4_add_cxx_unit_test_white(integer_white util)
+cvc4_add_cxx_unit_test_black(output_black util)
+cvc4_add_cxx_unit_test_black(rational_black util)
+cvc4_add_cxx_unit_test_white(rational_white util)
 if(CVC4_USE_POLY_IMP)
-cvc4_add_unit_test_black(real_algebraic_number_black util)
+cvc4_add_cxx_unit_test_black(real_algebraic_number_black util)
 endif()
-cvc4_add_unit_test_black(stats_black util)
+cvc4_add_cxx_unit_test_black(stats_black util)