Merge branch 'master' into fixConfigureTypofixConfigureTypo

13 files changed, 313 insertions, 312 deletions

diff --git a/test/unit/.gitignore b/test/unit/.gitignore
deleted file mode 100644
index 77b1fc5e3..000000000
--- a/test/unit/.gitignore
+++ /dev/null
@@ -1,4 +0,0 @@
-*_black
-*_white
-*_black.cpp
-*_white.cpp
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index 7c8e3d766..4ba7205a5 100644
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -49,6 +49,7 @@ macro(cvc4_add_unit_test is_white name output_dir)
   # As a consequence, all build target names must be globally unique.
   add_executable(${name} ${test_src} ${test_header})
   target_link_libraries(${name} main-test)
+  target_include_directories(${name} PRIVATE ${CxxTest_INCLUDE_DIR})
   target_compile_definitions(${name} PRIVATE ${CVC4_CXXTEST_FLAGS_BLACK})
   if(${is_white})
     target_compile_options(${name} PRIVATE -fno-access-control)
diff --git a/test/unit/Makefile b/test/unit/Makefile
deleted file mode 100644
index 16dc971e1..000000000
--- a/test/unit/Makefile
+++ /dev/null
@@ -1,8 +0,0 @@
-topdir = ../..
-srcdir = test/unit
-
-include $(topdir)/Makefile.subdir
-
-# synonyms for "check"
-.PHONY: test
-test: check
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
deleted file mode 100644
index 0ce6368c2..000000000
--- a/test/unit/Makefile.am
+++ /dev/null
@@ -1,248 +0,0 @@
-# All unit tests
-UNIT_TESTS = \
-	expr/expr_public \
-	expr/expr_manager_public \
-	expr/type_cardinality_public \
-	util/cardinality_public
-if WHITE_AND_BLACK_TESTS
-UNIT_TESTS += \
-	base/map_util_black \
-	theory/evaluator_white \
-	theory/logic_info_white \
-	theory/theory_arith_white \
-	theory/theory_black \
-	theory/theory_bv_white \
-	theory/theory_engine_white \
-	theory/theory_quantifiers_bv_instantiator_white \
-	theory/theory_quantifiers_bv_inverter_white \
-	theory/theory_strings_rewriter_white \
-	theory/theory_white \
-	theory/type_enumerator_white \
-	expr/node_white \
-	expr/node_black \
-	expr/kind_black \
-	expr/kind_map_black \
-	expr/node_builder_black \
-	expr/node_manager_black \
-	expr/node_manager_white \
-	expr/attribute_white \
-	expr/attribute_black \
-	expr/symbol_table_black \
-	expr/node_self_iterator_black \
-	expr/type_node_white \
-	parser/parser_black \
-	parser/parser_builder_black \
-	preprocessing/pass_bv_gauss_white \
-	prop/cnf_stream_white \
-	context/context_black \
-	context/context_white \
-	context/context_mm_black \
-	context/cdo_black \
-	context/cdlist_black \
-	context/cdmap_black \
-	context/cdmap_white \
-	util/array_store_all_black \
-	util/assert_white \
-	util/check_white \
-	util/binary_heap_black \
-	util/bitvector_black \
-	util/datatype_black \
-	util/configuration_black \
-	util/output_black \
-	util/exception_black \
-	util/integer_black \
-	util/integer_white \
-	util/listener_black \
-	util/rational_black \
-	util/rational_white \
-	util/stats_black \
-	util/boolean_simplification_black \
-	main/interactive_shell_black
-endif
-
-export VERBOSE = 1
-
-# Things that aren't tests but that tests rely on and need to
-# go into the distribution
-TEST_DEPS_DIST = \
-	memory.h \
-	Makefile.tests
-
-if HAVE_CXXTESTGEN
-
-AM_CPPFLAGS = \
-	-I. \
-	"-I@top_builddir@/src" \
-	"-I@top_srcdir@/src/include" \
-	"-I@top_srcdir@/lib" \
-	"-I@top_srcdir@/src" \
-	"-I@top_srcdir@/src/prop/minisat" \
-	-D __STDC_LIMIT_MACROS \
-	-D __STDC_FORMAT_MACROS \
-	$(ANTLR_INCLUDES) \
-	$(TEST_CPPFLAGS)
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(TEST_CXXFLAGS)
-AM_LDFLAGS = $(TEST_LDFLAGS) $(READLINE_LIBS) $(LIBS)
-CXXFLAGS=-Wno-suggest-override
-
-AM_CXXFLAGS_WHITE = -fno-access-control -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST
-AM_CXXFLAGS_BLACK = -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST
-AM_CXXFLAGS_PUBLIC =
-AM_LDFLAGS_WHITE =
-AM_LDFLAGS_BLACK =
-AM_LDFLAGS_PUBLIC =
-AM_LIBADD_WHITE = \
-	@abs_top_builddir@/src/main/libmain.a \
-	@abs_top_builddir@/src/parser/libcvc4parser.la \
-	@abs_top_builddir@/src/libcvc4.la
-AM_LIBADD_BLACK = \
-	@abs_top_builddir@/src/main/libmain.a \
-	@abs_top_builddir@/src/parser/libcvc4parser.la \
-	@abs_top_builddir@/src/libcvc4.la
-AM_LIBADD_PUBLIC = \
-	@abs_top_builddir@/src/parser/libcvc4parser.la \
-	@abs_top_builddir@/src/libcvc4.la
-
-EXTRA_DIST = \
-	no_cxxtest \
-	$(UNIT_TESTS:%=%.cpp) \
-	$(UNIT_TESTS:%=%.h) \
-	$(TEST_DEPS_DIST)
-
-MOSTLYCLEANFILES = $(UNIT_TESTS) $(UNIT_TESTS:%=%.cpp) $(UNIT_TESTS:%=%.lo)
-DISTCLEANFILES = $(UNIT_TESTS:%=@DEPDIR@/%.Plo)
-
-# the tests automake infrastructure doesn't clean up .o files :-(
-# handle both .libs and _libs variants
-mostlyclean-local:
-	@for f in $(UNIT_TESTS); do \
-		dir="$$(dirname "$$f")"; fil="$$(basename "$$f")"; \
-		for junk in	"$$dir/.libs/$$fil.o" \
-				"$$dir/_libs/$$fil.o" \
-				"$$dir/.libs/lt-$$fil" \
-				"$$dir/_libs/lt-$$fil" \
-				"$$dir/.libs/$$fil" \
-				"$$dir/_libs/$$fil"; do \
-			if test -e "$$junk"; then \
-				echo "rm -f \"$$junk\""; \
-				rm -f "$$junk"; \
-			fi; \
-		done; \
-	done
-
-@mk_include@ @srcdir@/Makefile.tests
-
-# We leave "TESTS" empty here; it's handled in Makefile.tests (see
-# that file for comment)
-TESTS = $(UNIT_TESTS)
-
-if STATIC_BINARY
-unit_LINK = $(CXXLINK) -all-static
-else
-unit_LINK = $(CXXLINK)
-endif
-
-@AMDEP_TRUE@@am__include@ $(UNIT_TESTS:%=@am__quote@./@DEPDIR@/%.Plo@am__quote@)
-
-$(UNIT_TESTS:%=@am__quote@./@DEPDIR@/%.Plo@am__quote@): %.Plo:
-	$(AM_V_at)$(MKDIR_P) `dirname "$@"`
-	$(AM_V_GEN)test -e "$@" || touch "$@"
-
-$(UNIT_TESTS:%=@abs_builddir@/%.cpp): @abs_builddir@/%.cpp: %.h
-	$(AM_V_at)$(MKDIR_P) `dirname "$@"`
-	$(AM_V_GEN)$(CXXTESTGEN) --no-static-init --have-eh --have-std --error-printer -o "$@" "$<"
-
-$(WHITE_TESTS:%=%.lo): %_white.lo: @abs_builddir@/%_white.cpp
-@am__fastdepCXX_TRUE@	$(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -MT $@ -MD -MP -MF $(DEPDIR)/$(@:%.lo=%).Tpo -c -o $@ $<
-@am__fastdepCXX_TRUE@	$(AM_V_at)$(am__mv) $(DEPDIR)/$(@:%.lo=%).Tpo $(DEPDIR)/$(@:%.lo=%).Plo
-@am__fastdepCXX_FALSE@	$(AM_V_CXX) @AM_BACKSLASH@
-@AMDEP_TRUE@@am__fastdepCXX_FALSE@	source='$<' object='$@' libtool=yes @AMDEPBACKSLASH@
-@AMDEP_TRUE@@am__fastdepCXX_FALSE@	DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
-@am__fastdepCXX_FALSE@	$(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@ $<
-
-$(WHITE_TESTS): %_white: %_white.lo $(AM_LIBADD_WHITE)
-	$(AM_V_CXXLD)$(unit_LINK) $(AM_LIBADD_WHITE) $(AM_LDFLAGS) $(AM_LDFLAGS_WHITE) $<
-
-$(BLACK_TESTS:%=%.lo): %_black.lo: @abs_builddir@/%_black.cpp
-@am__fastdepCXX_TRUE@	$(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -MT $@ -MD -MP -MF $(DEPDIR)/$(@:%.lo=%).Tpo -c -o $@ $<
-@am__fastdepCXX_TRUE@	$(AM_V_at)$(am__mv) $(DEPDIR)/$(@:%.lo=%).Tpo $(DEPDIR)/$(@:%.lo=%).Plo
-@am__fastdepCXX_FALSE@	$(AM_V_CXX) @AM_BACKSLASH@
-@AMDEP_TRUE@@am__fastdepCXX_FALSE@	source='$<' object='$@' libtool=yes @AMDEPBACKSLASH@
-@AMDEP_TRUE@@am__fastdepCXX_FALSE@	DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
-@am__fastdepCXX_FALSE@	$(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@ $<
-
-$(BLACK_TESTS): %_black: %_black.lo $(AM_LIBADD_BLACK)
-	$(AM_V_CXXLD)$(unit_LINK) $(AM_LIBADD_BLACK) $(AM_LDFLAGS) $(AM_LDFLAGS_BLACK) $<
-
-$(PUBLIC_TESTS:%=%.lo): %_public.lo: @abs_builddir@/%_public.cpp
-@am__fastdepCXX_TRUE@	$(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -MT $@ -MD -MP -MF $(DEPDIR)/$(@:%.lo=%).Tpo -c -o $@ $<
-@am__fastdepCXX_TRUE@	$(AM_V_at)$(am__mv) $(DEPDIR)/$(@:%.lo=%).Tpo $(DEPDIR)/$(@:%.lo=%).Plo
-@am__fastdepCXX_FALSE@	$(AM_V_CXX) @AM_BACKSLASH@
-@AMDEP_TRUE@@am__fastdepCXX_FALSE@	source='$<' object='$@' libtool=yes @AMDEPBACKSLASH@
-@AMDEP_TRUE@@am__fastdepCXX_FALSE@	DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
-@am__fastdepCXX_FALSE@	$(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@ $<
-
-$(PUBLIC_TESTS): %_public: %_public.lo $(AM_LIBADD_PUBLIC)
-	$(AM_V_CXXLD)$(unit_LINK) $(AM_LIBADD_PUBLIC) $(AM_LDFLAGS) $(AM_LDFLAGS_PUBLIC) $<
-
-else
-
-# force a user-visible failure for "make check"
-TESTS = no_cxxtest
-
-EXTRA_DIST = \
-	no_cxxtest \
-	$(UNIT_TESTS:%=%.h) \
-	$(TEST_DEPS_DIST) \
-	no-cxxtest-available
-
-endif
-
-$(UNIT_TESTS:%=%.cpp): $(UNIT_TESTS:%=@abs_builddir@/%.cpp)
-
-# trick automake into setting LTCXXCOMPILE, CXXLINK, etc.
-if CVC4_FALSE
-noinst_LTLIBRARIES = libdummy.la
-nodist_libdummy_la_SOURCES = expr/node_black.cpp
-libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la
-endif
-
-# synonyms for "check" in this directory in this directory
-.PHONY: units test
-units test: check
-
-# no-ops here
-.PHONY: systemtests regress regress0 regress1 regress2 regress3 regress4
-regress regress0 regress1 regress2 regress3 regress4:
-
-if HAVE_CXXTESTGEN
-# all is fine with the world
-else
-# all is not !
-no-cxxtest-available:
-	@if test "$(I_REALLY_WANT_TO_BUILD_CVC4_DIST_WITHOUT_TESTS)" = 1; then \
-		echo; \
-		echo "WARNING:"; \
-		echo "WARNING: No CxxTest to build unit tests, but, then, you know that;"; \
-		echo "WARNING: I hope you know what you're doing."; \
-		echo "WARNING:"; \
-		echo; \
-		( echo "CxxTest was not available at the time this distribution was built,"; \
-		  echo "so the tests could not be built.  You'll need CxxTest to test this"; \
-		  echo "distribution." ) >no-cxxtest-available; \
-	else \
-		echo; \
-		echo "ERROR:"; \
-		echo "ERROR: You cannot make dist in this build directory, you do not have CxxTest."; \
-		echo "ERROR: The tests should be generated for the user and included in the tarball,"; \
-		echo "ERROR: otherwise they'll be required to have CxxTest just to test the standard"; \
-		echo "ERROR: distribution built correctly."; \
-		echo "ERROR: If you really want to do this, append the following to your make command."; \
-		echo "ERROR:"; \
-		echo "ERROR:     I_REALLY_WANT_TO_BUILD_CVC4_DIST_WITHOUT_TESTS=1"; \
-		echo "ERROR:"; \
-		echo; \
-		exit 1; \
-	fi >&2
-endif
-
diff --git a/test/unit/Makefile.tests b/test/unit/Makefile.tests
deleted file mode 100644
index e3ec536ce..000000000
--- a/test/unit/Makefile.tests
+++ /dev/null
@@ -1,20 +0,0 @@
-# This makefile is separated because it's not under automake control.
-# This gets confusing, because we want:
-#
-#  1. to (re)build only the tests in the "filtered" set of tests
-#     (those that we're going to run)
-#  2. run only the tests in the "filtered" set of tests.
-#
-# It's a pain to make automake happy.
-
-# Add "filtered" tests to the set of TESTS
-TESTS = $(filter $(TEST_PREFIX)%,$(filter %$(TEST_SUFFIX),$(UNIT_TESTS)))
-
-# subsets of the tests, based on name
-WHITE_TESTS = $(filter %_white,$(UNIT_TESTS))
-BLACK_TESTS = $(filter %_black,$(UNIT_TESTS))
-PUBLIC_TESTS = $(filter %_public,$(UNIT_TESTS))
-
-# This rule forces automake to correctly build our filtered
-# set of tests
-check-TESTS: $(TESTS)
diff --git a/test/unit/memory.h b/test/unit/memory.h
index a4d650b3b..8f4eca371 100644
--- a/test/unit/memory.h
+++ b/test/unit/memory.h
@@ -36,6 +36,7 @@
 #include <sys/resource.h>
 #include <sys/time.h>
 
+#include "base/configuration_private.h"
 #include "base/cvc4_assert.h"
 
 // Conditionally define CVC4_MEMORY_LIMITING_DISABLED.
@@ -43,29 +44,15 @@
 #  define CVC4_MEMORY_LIMITING_DISABLED 1
 #  define CVC4_MEMORY_LIMITING_DISABLED_REASON "setrlimit() is broken on Mac."
 #else /* __APPLE__ */
-// Clang test
-#  if defined(__has_feature)
-#    if __has_feature(address_sanitizer)
-#      define _IS_ASAN_BUILD
-#    endif /* __has_feature(address_sanitizer) */
-#  endif /* defined(__has_feature) */
-
-// GCC test
-#  if defined(__SANITIZE_ADDRESS__)
-#    define _IS_ASAN_BUILD
-#  endif /* defined(__SANITIZE_ADDRESS__) */
 
 // Tests cannot expect bad_alloc to be thrown due to limit memory using
 // setrlimit when ASAN is enable. ASAN instead aborts on mmap failures.
-#  if defined(_IS_ASAN_BUILD)
+#  if IS_ASAN_BUILD
 #    define CVC4_MEMORY_LIMITING_DISABLED 1
 #    define CVC4_MEMORY_LIMITING_DISABLED_REASON "ASAN's mmap failures abort."
-#    undef _IS_ASAN_BUILD
-#  endif /* defined(_IS_ASAN_BUILD) */
+#  endif
 #endif
 
-
-
 namespace CVC4 {
 namespace test {
 
diff --git a/test/unit/no_cxxtest b/test/unit/no_cxxtest
deleted file mode 100755
index fec2dfb82..000000000
--- a/test/unit/no_cxxtest
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/bin/sh
-
-echo
-echo '***************************************************************************'
-echo '*                                                                         *'
-echo '*  WARNING:  CxxTest not found at configure time; unit tests cannot run.  *'
-echo '*                                                                         *'
-echo '***************************************************************************'
-echo
-
-# skip this test, rather than reporting an error
-exit 77
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index 7e04bb7c5..35eb240a2 100644
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -136,6 +136,10 @@ class CnfStreamWhite : public CxxTest::TestSuite {
     d_nodeManager = NodeManager::fromExprManager(d_exprManager);
     d_scope = new SmtScope(d_smt);
 
+    // Notice that this unit test uses the theory engine of a created SMT
+    // engine d_smt. We must ensure that d_smt is properly initialized via
+    // the following call, which constructs its underlying theory engine.
+    d_smt->finalOptionsAreSet();
     d_theoryEngine = d_smt->d_theoryEngine;
 
     d_satSolver = new FakeSatSolver();
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index 7661c08b5..d81406dac 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -109,6 +109,11 @@ public:
     d_outputChannel.clear();
     d_logicInfo.lock();
 
+    // Notice that this unit test uses the theory engine of a created SMT
+    // engine d_smt. We must ensure that d_smt is properly initialized via
+    // the following call, which constructs its underlying theory engine.
+    d_smt->finalOptionsAreSet();
+
     // guard against duplicate statistics assertion errors
     delete d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH];
     delete d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH];
diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h
index bc5b36a0b..9b0d56998 100644
--- a/test/unit/theory/theory_bv_white.h
+++ b/test/unit/theory/theory_bv_white.h
@@ -70,6 +70,10 @@ public:
   void testBitblasterCore() {
     d_smt->setOption("bitblast", SExpr("eager"));
     d_smt->setOption("incremental", SExpr("false"));
+    // Notice that this unit test uses the theory engine of a created SMT
+    // engine d_smt. We must ensure that d_smt is properly initialized via
+    // the following call, which constructs its underlying theory engine.
+    d_smt->finalOptionsAreSet();
     EagerBitblaster* bb = new EagerBitblaster(
         dynamic_cast<TheoryBV*>(
             d_smt->d_theoryEngine->d_theoryTable[THEORY_BV]),
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 620fcd92e..50057f9fd 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -251,6 +251,10 @@ public:
 
     d_nullChannel = new FakeOutputChannel();
 
+    // Notice that this unit test uses the theory engine of a created SMT
+    // engine d_smt. We must ensure that d_smt is properly initialized via
+    // the following call, which constructs its underlying theory engine.
+    d_smt->finalOptionsAreSet();
     d_theoryEngine = d_smt->d_theoryEngine;
     for(TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id) {
       delete d_theoryEngine->d_theoryOut[id];
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index d038b310e..87aef3704 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -80,6 +80,61 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     TS_ASSERT_DIFFERS(res_t1, res_t2);
   }
 
+  void testCheckEntailLengthOne()
+  {
+    TypeNode intType = d_nm->integerType();
+    TypeNode strType = d_nm->stringType();
+
+    Node a = d_nm->mkConst(::CVC4::String("A"));
+    Node abcd = d_nm->mkConst(::CVC4::String("ABCD"));
+    Node aaad = d_nm->mkConst(::CVC4::String("AAAD"));
+    Node b = d_nm->mkConst(::CVC4::String("B"));
+    Node x = d_nm->mkVar("x", strType);
+    Node y = d_nm->mkVar("y", strType);
+    Node negOne = d_nm->mkConst(Rational(-1));
+    Node zero = d_nm->mkConst(Rational(0));
+    Node one = d_nm->mkConst(Rational(1));
+    Node two = d_nm->mkConst(Rational(2));
+    Node three = d_nm->mkConst(Rational(3));
+    Node i = d_nm->mkVar("i", intType);
+
+    TS_ASSERT(TheoryStringsRewriter::checkEntailLengthOne(a));
+    TS_ASSERT(TheoryStringsRewriter::checkEntailLengthOne(a, true));
+
+    Node substr = d_nm->mkNode(kind::STRING_SUBSTR, x, zero, one);
+    TS_ASSERT(TheoryStringsRewriter::checkEntailLengthOne(substr));
+    TS_ASSERT(!TheoryStringsRewriter::checkEntailLengthOne(substr, true));
+
+    substr = d_nm->mkNode(kind::STRING_SUBSTR,
+                          d_nm->mkNode(kind::STRING_CONCAT, a, x),
+                          zero,
+                          one);
+    TS_ASSERT(TheoryStringsRewriter::checkEntailLengthOne(substr));
+    TS_ASSERT(TheoryStringsRewriter::checkEntailLengthOne(substr, true));
+
+    substr = d_nm->mkNode(kind::STRING_SUBSTR, x, zero, two);
+    TS_ASSERT(!TheoryStringsRewriter::checkEntailLengthOne(substr));
+    TS_ASSERT(!TheoryStringsRewriter::checkEntailLengthOne(substr, true));
+  }
+
+  void testCheckEntailArith()
+  {
+    TypeNode intType = d_nm->integerType();
+    TypeNode strType = d_nm->stringType();
+
+    Node z = d_nm->mkVar("z", strType);
+    Node n = d_nm->mkVar("n", intType);
+    Node one = d_nm->mkConst(Rational(1));
+
+    // 1 >= (str.len (str.substr z n 1)) ---> true
+    Node substr_z = d_nm->mkNode(kind::STRING_LENGTH,
+                                 d_nm->mkNode(kind::STRING_SUBSTR, z, n, one));
+    TS_ASSERT(TheoryStringsRewriter::checkEntailArith(one, substr_z));
+
+    // (str.len (str.substr z n 1)) >= 1 ---> false
+    TS_ASSERT(!TheoryStringsRewriter::checkEntailArith(substr_z, one));
+  }
+
   void testCheckEntailArithWithAssumption()
   {
     TypeNode intType = d_nm->integerType();
@@ -90,6 +145,10 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     Node z = d_nm->mkVar("z", intType);
 
     Node zero = d_nm->mkConst(Rational(0));
+    Node one = d_nm->mkConst(Rational(1));
+
+    Node empty = d_nm->mkConst(::CVC4::String(""));
+    Node a = d_nm->mkConst(::CVC4::String("A"));
 
     Node slen_y = d_nm->mkNode(kind::STRING_LENGTH, y);
     Node x_plus_slen_y = d_nm->mkNode(kind::PLUS, x, slen_y);
@@ -143,6 +202,14 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     // x + 5 < 5 |= 0 > x --> true
     TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption(
         x_plus_five_lt_five, zero, x, false));
+
+    // 0 < x |= x >= (str.len (int.to.str x))
+    Node assm = Rewriter::rewrite(d_nm->mkNode(kind::LT, zero, x));
+    TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption(
+        assm,
+        x,
+        d_nm->mkNode(kind::STRING_LENGTH, d_nm->mkNode(kind::STRING_ITOS, x)),
+        false));
   }
 
   void testRewriteSubstr()
@@ -152,11 +219,15 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
 
     Node empty = d_nm->mkConst(::CVC4::String(""));
     Node a = d_nm->mkConst(::CVC4::String("A"));
+    Node b = d_nm->mkConst(::CVC4::String("B"));
     Node abcd = d_nm->mkConst(::CVC4::String("ABCD"));
+    Node zero = d_nm->mkConst(Rational(0));
+    Node one = d_nm->mkConst(Rational(1));
     Node two = d_nm->mkConst(Rational(2));
     Node three = d_nm->mkConst(Rational(3));
 
     Node s = d_nm->mkVar("s", strType);
+    Node s2 = d_nm->mkVar("s2", strType);
     Node x = d_nm->mkVar("x", intType);
     Node y = d_nm->mkVar("y", intType);
 
@@ -198,6 +269,67 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
         kind::STRING_SUBSTR, abcd, d_nm->mkNode(kind::PLUS, x, two), x);
     res = TheoryStringsRewriter::rewriteSubstr(n);
     TS_ASSERT_EQUALS(res, n);
+
+    // (str.substr (str.substr s x x) x x) -> ""
+    n = d_nm->mkNode(
+        kind::STRING_SUBSTR, d_nm->mkNode(kind::STRING_SUBSTR, s, x, x), x, x);
+    sameNormalForm(n, empty);
+
+    // Same normal form for:
+    //
+    // (str.substr (str.replace "" s "B") x x)
+    //
+    // (str.replace "" s (str.substr "B" x x)))
+    Node lhs = d_nm->mkNode(kind::STRING_SUBSTR,
+                            d_nm->mkNode(kind::STRING_STRREPL, empty, s, b),
+                            x,
+                            x);
+    Node rhs = d_nm->mkNode(kind::STRING_STRREPL,
+                            empty,
+                            s,
+                            d_nm->mkNode(kind::STRING_SUBSTR, b, x, x));
+    sameNormalForm(lhs, rhs);
+
+    // Same normal form:
+    //
+    // (str.substr (str.replace s "A" "B") 0 x)
+    //
+    // (str.replace (str.substr s 0 x) "A" "B")
+    Node substr_repl = d_nm->mkNode(kind::STRING_SUBSTR,
+                                    d_nm->mkNode(kind::STRING_STRREPL, s, a, b),
+                                    zero,
+                                    x);
+    Node repl_substr =
+        d_nm->mkNode(kind::STRING_STRREPL,
+                     d_nm->mkNode(kind::STRING_SUBSTR, s, zero, x),
+                     a,
+                     b);
+    sameNormalForm(substr_repl, repl_substr);
+
+    // Same normal form:
+    //
+    // (str.substr (str.replace s (str.substr (str.++ s2 "A") 0 1) "B") 0 x)
+    //
+    // (str.replace (str.substr s 0 x) (str.substr (str.++ s2 "A") 0 1) "B")
+    Node substr_y = d_nm->mkNode(kind::STRING_SUBSTR,
+                                 d_nm->mkNode(kind::STRING_CONCAT, s2, a),
+                                 zero,
+                                 one);
+    substr_repl =
+        d_nm->mkNode(kind::STRING_SUBSTR,
+                     d_nm->mkNode(kind::STRING_STRREPL, s, substr_y, b),
+                     zero,
+                     x);
+    repl_substr = d_nm->mkNode(kind::STRING_STRREPL,
+                               d_nm->mkNode(kind::STRING_SUBSTR, s, zero, x),
+                               substr_y,
+                               b);
+    sameNormalForm(substr_repl, repl_substr);
+
+    // (str.substr (str.int.to.str x) x x) ---> empty
+    Node substr_itos = d_nm->mkNode(
+        kind::STRING_SUBSTR, d_nm->mkNode(kind::STRING_ITOS, x), x, x);
+    sameNormalForm(substr_itos, empty);
   }
 
   void testRewriteConcat()
@@ -297,6 +429,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
 
   void testRewriteIndexOf()
   {
+    TypeNode intType = d_nm->integerType();
     TypeNode strType = d_nm->stringType();
 
     Node a = d_nm->mkConst(::CVC4::String("A"));
@@ -305,17 +438,20 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     Node b = d_nm->mkConst(::CVC4::String("B"));
     Node x = d_nm->mkVar("x", strType);
     Node y = d_nm->mkVar("y", strType);
-    Node one = d_nm->mkConst(Rational(2));
+    Node negOne = d_nm->mkConst(Rational(-1));
+    Node one = d_nm->mkConst(Rational(1));
+    Node two = d_nm->mkConst(Rational(2));
     Node three = d_nm->mkConst(Rational(3));
+    Node i = d_nm->mkVar("i", intType);
 
     // Same normal form for:
     //
     // (str.to.int (str.indexof "A" x 1))
     //
     // (str.to.int (str.indexof "B" x 1))
-    Node a_idof_x = d_nm->mkNode(kind::STRING_STRIDOF, a, x, one);
+    Node a_idof_x = d_nm->mkNode(kind::STRING_STRIDOF, a, x, two);
     Node itos_a_idof_x = d_nm->mkNode(kind::STRING_ITOS, a_idof_x);
-    Node b_idof_x = d_nm->mkNode(kind::STRING_STRIDOF, b, x, one);
+    Node b_idof_x = d_nm->mkNode(kind::STRING_STRIDOF, b, x, two);
     Node itos_b_idof_x = d_nm->mkNode(kind::STRING_ITOS, b_idof_x);
     sameNormalForm(itos_a_idof_x, itos_b_idof_x);
 
@@ -333,10 +469,19 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
                                   y,
                                   three);
     sameNormalForm(idof_abcd, idof_aaad);
+
+    // (str.indexof (str.substr x 1 i) "A" i) ---> -1
+    Node idof_substr =
+        d_nm->mkNode(kind::STRING_STRIDOF,
+                     d_nm->mkNode(kind::STRING_SUBSTR, x, one, i),
+                     a,
+                     i);
+    sameNormalForm(idof_substr, negOne);
   }
 
   void testRewriteReplace()
   {
+    TypeNode intType = d_nm->integerType();
     TypeNode strType = d_nm->stringType();
 
     Node empty = d_nm->mkConst(::CVC4::String(""));
@@ -347,6 +492,9 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     Node x = d_nm->mkVar("x", strType);
     Node y = d_nm->mkVar("y", strType);
     Node z = d_nm->mkVar("z", strType);
+    Node zero = d_nm->mkConst(Rational(0));
+    Node one = d_nm->mkConst(Rational(1));
+    Node n = d_nm->mkVar("n", intType);
 
     // (str.replace (str.replace x "B" x) x "A") -->
     //   (str.replace (str.replace x "B" "A") x "A")
@@ -418,6 +566,44 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
                              d_nm->mkNode(kind::STRING_STRREPL, y, x, a),
                              y);
     sameNormalForm(repl_repl, empty);
+
+    // (str.replace "" (str.replace x y x) x) ---> ""
+    repl_repl = d_nm->mkNode(kind::STRING_STRREPL,
+                             empty,
+                             d_nm->mkNode(kind::STRING_STRREPL, x, y, x),
+                             x);
+    sameNormalForm(repl_repl, empty);
+
+    // (str.replace "" (str.substr x 0 1) x) ---> ""
+    repl_repl = d_nm->mkNode(kind::STRING_STRREPL,
+                             empty,
+                             d_nm->mkNode(kind::STRING_SUBSTR, x, zero, one),
+                             x);
+    sameNormalForm(repl_repl, empty);
+
+    // Same normal form for:
+    //
+    // (str.replace "" (str.replace x y x) y)
+    //
+    // (str.replace "" x y)
+    repl_repl = d_nm->mkNode(kind::STRING_STRREPL,
+                             empty,
+                             d_nm->mkNode(kind::STRING_STRREPL, x, y, x),
+                             y);
+    Node repl = d_nm->mkNode(kind::STRING_STRREPL, empty, x, y);
+    sameNormalForm(repl_repl, repl);
+
+    // Same normal form:
+    //
+    // (str.replace "B" (str.replace x "A" "B") "B")
+    //
+    // (str.replace "B" x "B"))
+    repl_repl = d_nm->mkNode(kind::STRING_STRREPL,
+                             b,
+                             d_nm->mkNode(kind::STRING_STRREPL, x, a, b),
+                             b);
+    repl = d_nm->mkNode(kind::STRING_STRREPL, b, x, b);
+    sameNormalForm(repl_repl, repl);
   }
 
   void testRewriteContains()
@@ -435,9 +621,11 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     Node yx = d_nm->mkNode(kind::STRING_CONCAT, y, x);
     Node z = d_nm->mkVar("z", strType);
     Node n = d_nm->mkVar("n", intType);
-    Node one = d_nm->mkConst(Rational(2));
+    Node one = d_nm->mkConst(Rational(1));
+    Node two = d_nm->mkConst(Rational(2));
     Node three = d_nm->mkConst(Rational(3));
     Node four = d_nm->mkConst(Rational(4));
+    Node t = d_nm->mkConst(true);
     Node f = d_nm->mkConst(false);
 
     // Same normal form for:
@@ -582,6 +770,81 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     Node ctn_yxxy = d_nm->mkNode(kind::STRING_STRCTN, yx, xy);
     Node eq_yxxy = d_nm->mkNode(kind::EQUAL, yx, xy);
     sameNormalForm(ctn_yxxy, eq_yxxy);
+
+    // (str.contains (str.replace x y x) x) ---> true
+    ctn_repl = d_nm->mkNode(
+        kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, y, x), x);
+    sameNormalForm(ctn_repl, t);
+
+    // (str.contains (str.replace (str.++ x y) z (str.++ y x)) x) ---> true
+    ctn_repl = d_nm->mkNode(
+        kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, xy, z, yx), x);
+    sameNormalForm(ctn_repl, t);
+
+    // (str.contains (str.++ z (str.replace (str.++ x y) z (str.++ y x))) x)
+    //   ---> true
+    ctn_repl = d_nm->mkNode(
+        kind::STRING_STRCTN,
+        d_nm->mkNode(kind::STRING_CONCAT,
+                     z,
+                     d_nm->mkNode(kind::STRING_STRREPL, xy, z, yx)),
+        x);
+    sameNormalForm(ctn_repl, t);
+
+    // Same normal form for:
+    //
+    // (str.contains (str.replace x y x) y)
+    //
+    // (str.contains x y)
+    Node lhs = d_nm->mkNode(
+        kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, y, x), y);
+    Node rhs = d_nm->mkNode(kind::STRING_STRCTN, x, y);
+    sameNormalForm(lhs, rhs);
+
+    // Same normal form for:
+    //
+    // (str.contains (str.replace x y x) "B")
+    //
+    // (str.contains x "B")
+    lhs = d_nm->mkNode(
+        kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, y, x), b);
+    rhs = d_nm->mkNode(kind::STRING_STRCTN, x, b);
+    sameNormalForm(lhs, rhs);
+
+    // Same normal form for:
+    //
+    // (str.contains (str.replace x y x) (str.substr z n 1))
+    //
+    // (str.contains x (str.substr z n 1))
+    Node substr_z = d_nm->mkNode(kind::STRING_SUBSTR, z, n, one);
+    lhs = d_nm->mkNode(kind::STRING_STRCTN,
+                       d_nm->mkNode(kind::STRING_STRREPL, x, y, x),
+                       substr_z);
+    rhs = d_nm->mkNode(kind::STRING_STRCTN, x, substr_z);
+    sameNormalForm(lhs, rhs);
+
+    // Same normal form for:
+    //
+    // (str.contains (str.replace x y z) z)
+    //
+    // (str.contains (str.replace x z y) y)
+    lhs = d_nm->mkNode(
+        kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, y, z), z);
+    rhs = d_nm->mkNode(
+        kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, z, y), y);
+    sameNormalForm(lhs, rhs);
+
+    // Same normal form for:
+    //
+    // (str.contains (str.replace x "A" "B") "A")
+    //
+    // (str.contains (str.replace x "A" "") "A")
+    lhs = d_nm->mkNode(
+        kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, a, b), a);
+    rhs = d_nm->mkNode(kind::STRING_STRCTN,
+                       d_nm->mkNode(kind::STRING_STRREPL, x, a, empty),
+                       a);
+    sameNormalForm(lhs, rhs);
   }
 
   void testInferEqsFromContains()
@@ -780,6 +1043,27 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     Node eq_xxa_repl_xxa = d_nm->mkNode(
         kind::EQUAL, xxa, d_nm->mkNode(kind::STRING_STRREPL, xxa, a, b));
     sameNormalForm(eq_xxa_repl_xxa, f);
+
+    // Same normal form for:
+    //
+    // (= (str.replace x "A" "B") "")
+    //
+    // (= x "")
+    Node eq_repl = d_nm->mkNode(
+        kind::EQUAL, d_nm->mkNode(kind::STRING_STRREPL, x, a, b), empty);
+    Node eq_x = d_nm->mkNode(kind::EQUAL, x, empty);
+    sameNormalForm(eq_repl, eq_x);
+
+    // Same normal form for:
+    //
+    // (= (str.replace y "A" "B") "B")
+    //
+    // (= (str.replace y "B" "A") "A")
+    Node lhs = d_nm->mkNode(
+        kind::EQUAL, d_nm->mkNode(kind::STRING_STRREPL, x, a, b), b);
+    Node rhs = d_nm->mkNode(
+        kind::EQUAL, d_nm->mkNode(kind::STRING_STRREPL, x, b, a), a);
+    sameNormalForm(lhs, rhs);
   }
 
  private:
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index c8265a755..4ff11014b 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -166,6 +166,10 @@ class TheoryBlack : public CxxTest::TestSuite {
     d_logicInfo = new LogicInfo();
     d_logicInfo->lock();
 
+    // Notice that this unit test uses the theory engine of a created SMT
+    // engine d_smt. We must ensure that d_smt is properly initialized via
+    // the following call, which constructs its underlying theory engine.
+    d_smt->finalOptionsAreSet();
     // guard against duplicate statistics assertion errors
     delete d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN];
     delete d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN];