hooking up the bitvector tests

39 files changed, 1791 insertions, 1 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index c376be91b..cdd347962 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,4 +1,4 @@
-SUBDIRS = . arith precedence uf
+SUBDIRS = . arith precedence uf bv
 
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
 MAKEFLAGS = -k
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
new file mode 100644
index 000000000..dd4246e16
--- /dev/null
+++ b/test/regress/regress0/bv/Makefile.am
@@ -0,0 +1,25 @@
+SUBDIRS = . core
+
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+MAKEFLAGS = -k
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+
+# Regression tests for SMT inputs
+SMT_TESTS = 
+
+# Regression tests for SMT2 inputs
+SMT2_TESTS = 
+
+# Regression tests for PL inputs
+CVC_TESTS = 
+
+# Regression tests derived from bug reports
+BUG_TESTS = 
+
+TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
+
+EXTRA_DIST = $(TESTS)
+
diff --git a/test/regress/regress0/bv/Makefile.in b/test/regress/regress0/bv/Makefile.in
new file mode 100644
index 000000000..bfcc5bd29
--- /dev/null
+++ b/test/regress/regress0/bv/Makefile.in
@@ -0,0 +1,893 @@
+# Makefile.in generated by automake 1.11.1 from Makefile.am.
+# @configure_input@
+
+# Copyright (C) 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001, 2002,
+# 2003, 2004, 2005, 2006, 2007, 2008, 2009  Free Software Foundation,
+# Inc.
+# This Makefile.in is free software; the Free Software Foundation
+# gives unlimited permission to copy and/or distribute it,
+# with or without modifications, as long as this notice is preserved.
+
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY, to the extent permitted by law; without
+# even the implied warranty of MERCHANTABILITY or FITNESS FOR A
+# PARTICULAR PURPOSE.
+
+@SET_MAKE@
+VPATH = @srcdir@
+pkgdatadir = $(datadir)/@PACKAGE@
+pkgincludedir = $(includedir)/@PACKAGE@
+pkglibdir = $(libdir)/@PACKAGE@
+pkglibexecdir = $(libexecdir)/@PACKAGE@
+am__cd = CDPATH="$${ZSH_VERSION+.}$(PATH_SEPARATOR)" && cd
+install_sh_DATA = $(install_sh) -c -m 644
+install_sh_PROGRAM = $(install_sh) -c
+install_sh_SCRIPT = $(install_sh) -c
+INSTALL_HEADER = $(INSTALL_DATA)
+transform = $(program_transform_name)
+NORMAL_INSTALL = :
+PRE_INSTALL = :
+POST_INSTALL = :
+NORMAL_UNINSTALL = :
+PRE_UNINSTALL = :
+POST_UNINSTALL = :
+build_triplet = @build@
+host_triplet = @host@
+target_triplet = @target@
+TESTS = $(am__EXEEXT_1) $(am__EXEEXT_1) $(am__EXEEXT_1) \
+	$(am__EXEEXT_1)
+subdir = test/regress/regress0/bv
+DIST_COMMON = $(srcdir)/Makefile.am $(srcdir)/Makefile.in
+ACLOCAL_M4 = $(top_srcdir)/aclocal.m4
+am__aclocal_m4_deps = $(top_srcdir)/config/antlr.m4 \
+	$(top_srcdir)/config/ax_prog_doxygen.m4 \
+	$(top_srcdir)/config/cvc4.m4 $(top_srcdir)/config/libtool.m4 \
+	$(top_srcdir)/config/ltoptions.m4 \
+	$(top_srcdir)/config/ltsugar.m4 \
+	$(top_srcdir)/config/ltversion.m4 \
+	$(top_srcdir)/config/lt~obsolete.m4 \
+	$(top_srcdir)/config/pkg.m4 $(top_srcdir)/configure.ac
+am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \
+	$(ACLOCAL_M4)
+mkinstalldirs = $(install_sh) -d
+CONFIG_HEADER = $(top_builddir)/cvc4autoconfig.h
+CONFIG_CLEAN_FILES =
+CONFIG_CLEAN_VPATH_FILES =
+AM_V_GEN = $(am__v_GEN_$(V))
+am__v_GEN_ = $(am__v_GEN_$(AM_DEFAULT_VERBOSITY))
+am__v_GEN_0 = @echo "  GEN   " $@;
+AM_V_at = $(am__v_at_$(V))
+am__v_at_ = $(am__v_at_$(AM_DEFAULT_VERBOSITY))
+am__v_at_0 = @
+SOURCES =
+DIST_SOURCES =
+RECURSIVE_TARGETS = all-recursive check-recursive dvi-recursive \
+	html-recursive info-recursive install-data-recursive \
+	install-dvi-recursive install-exec-recursive \
+	install-html-recursive install-info-recursive \
+	install-pdf-recursive install-ps-recursive install-recursive \
+	installcheck-recursive installdirs-recursive pdf-recursive \
+	ps-recursive uninstall-recursive
+RECURSIVE_CLEAN_TARGETS = mostlyclean-recursive clean-recursive	\
+  distclean-recursive maintainer-clean-recursive
+AM_RECURSIVE_TARGETS = $(RECURSIVE_TARGETS:-recursive=) \
+	$(RECURSIVE_CLEAN_TARGETS:-recursive=) tags TAGS ctags CTAGS \
+	check check-html recheck recheck-html distdir
+ETAGS = etags
+CTAGS = ctags
+# If stdout is a non-dumb tty, use colors.  If test -t is not supported,
+# then this fails; a conservative approach.  Of course do not redirect
+# stdout here, just stderr.
+am__tty_colors = \
+red=; grn=; lgn=; blu=; std=; \
+test "X$(AM_COLOR_TESTS)" != Xno \
+&& test "X$$TERM" != Xdumb \
+&& { test "X$(AM_COLOR_TESTS)" = Xalways || test -t 1 2>/dev/null; } \
+&& { \
+  red=''; \
+  grn=''; \
+  lgn=''; \
+  blu=''; \
+  std=''; \
+}
+am__vpath_adj_setup = srcdirstrip=`echo "$(srcdir)" | sed 's|.|.|g'`;
+am__vpath_adj = case $$p in \
+    $(srcdir)/*) f=`echo "$$p" | sed "s|^$$srcdirstrip/||"`;; \
+    *) f=$$p;; \
+  esac;
+am__strip_dir = f=`echo $$p | sed -e 's|^.*/||'`;
+am__install_max = 40
+am__nobase_strip_setup = \
+  srcdirstrip=`echo "$(srcdir)" | sed 's/[].[^$$\\*|]/\\\\&/g'`
+am__nobase_strip = \
+  for p in $$list; do echo "$$p"; done | sed -e "s|$$srcdirstrip/||"
+am__nobase_list = $(am__nobase_strip_setup); \
+  for p in $$list; do echo "$$p $$p"; done | \
+  sed "s| $$srcdirstrip/| |;"' / .*\//!s/ .*/ ./; s,\( .*\)/[^/]*$$,\1,' | \
+  $(AWK) 'BEGIN { files["."] = "" } { files[$$2] = files[$$2] " " $$1; \
+    if (++n[$$2] == $(am__install_max)) \
+      { print $$2, files[$$2]; n[$$2] = 0; files[$$2] = "" } } \
+    END { for (dir in files) print dir, files[dir] }'
+am__base_list = \
+  sed '$$!N;$$!N;$$!N;$$!N;$$!N;$$!N;$$!N;s/\n/ /g' | \
+  sed '$$!N;$$!N;$$!N;$$!N;s/\n/ /g'
+# Restructured Text title and section.
+am__rst_title = sed 's/.*/   &   /;h;s/./=/g;p;x;p;g;p;s/.*//'
+am__rst_section = sed 'p;s/./=/g;p;g'
+# Put stdin (possibly several lines separated by ".  ") in a box.
+am__text_box = $(AWK) '{				\
+  n = split($$0, lines, "\\.  "); max = 0;		\
+  for (i = 1; i <= n; ++i)				\
+    if (max < length(lines[i]))				\
+      max = length(lines[i]);				\
+  for (i = 0; i < max; ++i) line = line "=";		\
+  print line;						\
+  for (i = 1; i <= n; ++i) if (lines[i]) print lines[i];\
+  print line;						\
+}'
+# Solaris 10 'make', and several other traditional 'make' implementations,
+# pass "-e" to $(SHELL).  This contradicts POSIX.  Work around the problem
+# by disabling -e (using the XSI extension "set +e") if it's set.
+am__sh_e_setup = case $$- in *e*) set +e;; esac
+# To be inserted before the command running the test.  Creates the
+# directory for the log if needed.  Stores in $dir the directory
+# containing $f, in $tst the test, in $log the log, and passes
+# TESTS_ENVIRONMENT.  Save and restore TERM around use of
+# TESTS_ENVIRONMENT, in case that unsets it.
+am__check_pre = \
+$(am__sh_e_setup);					\
+$(am__vpath_adj_setup) $(am__vpath_adj)			\
+srcdir=$(srcdir); export srcdir;			\
+rm -f $@-t;						\
+trap 'st=$$?; rm -f '\''$(abs_builddir)/$@-t'\''; (exit $$st); exit $$st' \
+  1 2 13 15;						\
+am__odir=`echo "./$@" | sed 's|/[^/]*$$||'`;		\
+test "x$$am__odir" = x. || $(MKDIR_P) "$$am__odir" || exit $$?;	\
+if test -f "./$$f"; then dir=./;			\
+elif test -f "$$f"; then dir=;				\
+else dir="$(srcdir)/"; fi;				\
+tst=$$dir$$f; log='$@'; __SAVED_TERM=$$TERM;		\
+$(TESTS_ENVIRONMENT)
+RECHECK_LOGS = $(TEST_LOGS)
+am__EXEEXT_1 =
+TEST_SUITE_LOG = test-suite.log
+TEST_SUITE_HTML = $(TEST_SUITE_LOG:.log=.html)
+TEST_EXTENSIONS = @EXEEXT@ .test
+am__test_logs1 = $(TESTS:=.log)
+am__test_logs2 = $(am__test_logs1:@EXEEXT@.log=.log)
+TEST_LOGS = $(am__test_logs2:.test.log=.log)
+TEST_LOG_COMPILE = $(TEST_LOG_COMPILER) $(AM_TEST_LOG_FLAGS) \
+	$(TEST_LOG_FLAGS)
+TEST_LOGS_TMP = $(TEST_LOGS:.log=.log-t)
+DIST_SUBDIRS = $(SUBDIRS)
+DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST)
+am__relativize = \
+  dir0=`pwd`; \
+  sed_first='s,^\([^/]*\)/.*$$,\1,'; \
+  sed_rest='s,^[^/]*/*,,'; \
+  sed_last='s,^.*/\([^/]*\)$$,\1,'; \
+  sed_butlast='s,/*[^/]*$$,,'; \
+  while test -n "$$dir1"; do \
+    first=`echo "$$dir1" | sed -e "$$sed_first"`; \
+    if test "$$first" != "."; then \
+      if test "$$first" = ".."; then \
+        dir2=`echo "$$dir0" | sed -e "$$sed_last"`/"$$dir2"; \
+        dir0=`echo "$$dir0" | sed -e "$$sed_butlast"`; \
+      else \
+        first2=`echo "$$dir2" | sed -e "$$sed_first"`; \
+        if test "$$first2" = "$$first"; then \
+          dir2=`echo "$$dir2" | sed -e "$$sed_rest"`; \
+        else \
+          dir2="../$$dir2"; \
+        fi; \
+        dir0="$$dir0"/"$$first"; \
+      fi; \
+    fi; \
+    dir1=`echo "$$dir1" | sed -e "$$sed_rest"`; \
+  done; \
+  reldir="$$dir2"
+ACLOCAL = @ACLOCAL@
+AMTAR = @AMTAR@
+AM_DEFAULT_VERBOSITY = @AM_DEFAULT_VERBOSITY@
+ANTLR = @ANTLR@
+ANTLR_HOME = @ANTLR_HOME@
+ANTLR_INCLUDES = @ANTLR_INCLUDES@
+ANTLR_LDFLAGS = @ANTLR_LDFLAGS@
+AR = @AR@
+AS = @AS@
+AUTOCONF = @AUTOCONF@
+AUTOHEADER = @AUTOHEADER@
+AUTOMAKE = @AUTOMAKE@
+AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
+CC = @CC@
+CCDEPMODE = @CCDEPMODE@
+CFLAGS = @CFLAGS@
+CLN_CFLAGS = @CLN_CFLAGS@
+CLN_LIBS = @CLN_LIBS@
+CPP = @CPP@
+CPPFLAGS = @CPPFLAGS@
+CVC4_LIBRARY_VERSION = @CVC4_LIBRARY_VERSION@
+CVC4_PARSER_LIBRARY_VERSION = @CVC4_PARSER_LIBRARY_VERSION@
+CVC4_USE_CLN_IMP = @CVC4_USE_CLN_IMP@
+CVC4_USE_GMP_IMP = @CVC4_USE_GMP_IMP@
+CXX = @CXX@
+CXXCPP = @CXXCPP@
+CXXDEPMODE = @CXXDEPMODE@
+CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
+CXXTESTGEN = @CXXTESTGEN@
+CYGPATH_W = @CYGPATH_W@
+DEFS = @DEFS@
+DEPDIR = @DEPDIR@
+DLLTOOL = @DLLTOOL@
+DOXYGEN_PAPER_SIZE = @DOXYGEN_PAPER_SIZE@
+DSYMUTIL = @DSYMUTIL@
+DUMPBIN = @DUMPBIN@
+DX_CONFIG = @DX_CONFIG@
+DX_DOCDIR = @DX_DOCDIR@
+DX_DOT = @DX_DOT@
+DX_DOXYGEN = @DX_DOXYGEN@
+DX_DVIPS = @DX_DVIPS@
+DX_EGREP = @DX_EGREP@
+DX_ENV = @DX_ENV@
+DX_FLAG_DX_CURRENT_FEATURE = @DX_FLAG_DX_CURRENT_FEATURE@
+DX_FLAG_chi = @DX_FLAG_chi@
+DX_FLAG_chm = @DX_FLAG_chm@
+DX_FLAG_doc = @DX_FLAG_doc@
+DX_FLAG_dot = @DX_FLAG_dot@
+DX_FLAG_html = @DX_FLAG_html@
+DX_FLAG_man = @DX_FLAG_man@
+DX_FLAG_pdf = @DX_FLAG_pdf@
+DX_FLAG_ps = @DX_FLAG_ps@
+DX_FLAG_rtf = @DX_FLAG_rtf@
+DX_FLAG_xml = @DX_FLAG_xml@
+DX_HHC = @DX_HHC@
+DX_LATEX = @DX_LATEX@
+DX_MAKEINDEX = @DX_MAKEINDEX@
+DX_PDFLATEX = @DX_PDFLATEX@
+DX_PERL = @DX_PERL@
+DX_PROJECT = @DX_PROJECT@
+ECHO_C = @ECHO_C@
+ECHO_N = @ECHO_N@
+ECHO_T = @ECHO_T@
+EGREP = @EGREP@
+EXEEXT = @EXEEXT@
+FGREP = @FGREP@
+FLAG_VISIBILITY_HIDDEN = @FLAG_VISIBILITY_HIDDEN@
+GREP = @GREP@
+INSTALL = @INSTALL@
+INSTALL_DATA = @INSTALL_DATA@
+INSTALL_PROGRAM = @INSTALL_PROGRAM@
+INSTALL_SCRIPT = @INSTALL_SCRIPT@
+INSTALL_STRIP_PROGRAM = @INSTALL_STRIP_PROGRAM@
+LD = @LD@
+LDFLAGS = @LDFLAGS@
+LIBOBJS = @LIBOBJS@
+LIBS = @LIBS@
+LIBTOOL = @LIBTOOL@
+LIPO = @LIPO@
+LN_S = @LN_S@
+LTLIBOBJS = @LTLIBOBJS@
+MAKEINFO = @MAKEINFO@
+MKDIR_P = @MKDIR_P@
+NM = @NM@
+NMEDIT = @NMEDIT@
+OBJDUMP = @OBJDUMP@
+OBJEXT = @OBJEXT@
+OTOOL = @OTOOL@
+OTOOL64 = @OTOOL64@
+PACKAGE = @PACKAGE@
+PACKAGE_BUGREPORT = @PACKAGE_BUGREPORT@
+PACKAGE_NAME = @PACKAGE_NAME@
+PACKAGE_STRING = @PACKAGE_STRING@
+PACKAGE_TARNAME = @PACKAGE_TARNAME@
+PACKAGE_URL = @PACKAGE_URL@
+PACKAGE_VERSION = @PACKAGE_VERSION@
+PATH_SEPARATOR = @PATH_SEPARATOR@
+PERL = @PERL@
+PKG_CONFIG = @PKG_CONFIG@
+RANLIB = @RANLIB@
+SED = @SED@
+SET_MAKE = @SET_MAKE@
+SHELL = @SHELL@
+STATIC_BINARY = @STATIC_BINARY@
+STRIP = @STRIP@
+TEST_CPPFLAGS = @TEST_CPPFLAGS@
+TEST_CXXFLAGS = @TEST_CXXFLAGS@
+TEST_LDFLAGS = @TEST_LDFLAGS@
+VERSION = @VERSION@
+abs_builddir = @abs_builddir@
+abs_srcdir = @abs_srcdir@
+abs_top_builddir = @abs_top_builddir@
+abs_top_srcdir = @abs_top_srcdir@
+ac_ct_CC = @ac_ct_CC@
+ac_ct_CXX = @ac_ct_CXX@
+ac_ct_DUMPBIN = @ac_ct_DUMPBIN@
+am__include = @am__include@
+am__leading_dot = @am__leading_dot@
+am__quote = @am__quote@
+am__tar = @am__tar@
+am__untar = @am__untar@
+bindir = @bindir@
+build = @build@
+build_alias = @build_alias@
+build_cpu = @build_cpu@
+build_os = @build_os@
+build_vendor = @build_vendor@
+builddir = @builddir@
+datadir = @datadir@
+datarootdir = @datarootdir@
+docdir = @docdir@
+dvidir = @dvidir@
+exec_prefix = @exec_prefix@
+host = @host@
+host_alias = @host_alias@
+host_cpu = @host_cpu@
+host_os = @host_os@
+host_vendor = @host_vendor@
+htmldir = @htmldir@
+includedir = @includedir@
+infodir = @infodir@
+install_sh = @install_sh@
+libdir = @libdir@
+libexecdir = @libexecdir@
+localedir = @localedir@
+localstatedir = @localstatedir@
+lt_ECHO = @lt_ECHO@
+mandir = @mandir@
+mk_include = @mk_include@
+mkdir_p = @mkdir_p@
+oldincludedir = @oldincludedir@
+pdfdir = @pdfdir@
+prefix = @prefix@
+program_transform_name = @program_transform_name@
+psdir = @psdir@
+sbindir = @sbindir@
+sharedstatedir = @sharedstatedir@
+srcdir = @srcdir@
+sysconfdir = @sysconfdir@
+target = @target@
+target_alias = @target_alias@
+target_cpu = @target_cpu@
+target_os = @target_os@
+target_vendor = @target_vendor@
+top_build_prefix = @top_build_prefix@
+top_builddir = @top_builddir@
+top_srcdir = @top_srcdir@
+SUBDIRS = . core
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+MAKEFLAGS = -k
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+
+# Regression tests for SMT inputs
+SMT_TESTS = 
+
+# Regression tests for SMT2 inputs
+SMT2_TESTS = 
+
+# Regression tests for PL inputs
+CVC_TESTS = 
+
+# Regression tests derived from bug reports
+BUG_TESTS = 
+EXTRA_DIST = $(TESTS)
+all: all-recursive
+
+.SUFFIXES:
+.SUFFIXES: .html .log .test .test$(EXEEXT)
+$(srcdir)/Makefile.in:  $(srcdir)/Makefile.am  $(am__configure_deps)
+	@for dep in $?; do \
+	  case '$(am__configure_deps)' in \
+	    *$$dep*) \
+	      ( cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh ) \
+	        && { if test -f $@; then exit 0; else break; fi; }; \
+	      exit 1;; \
+	  esac; \
+	done; \
+	echo ' cd $(top_srcdir) && $(AUTOMAKE) --gnu test/regress/regress0/bv/Makefile'; \
+	$(am__cd) $(top_srcdir) && \
+	  $(AUTOMAKE) --gnu test/regress/regress0/bv/Makefile
+.PRECIOUS: Makefile
+Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status
+	@case '$?' in \
+	  *config.status*) \
+	    cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh;; \
+	  *) \
+	    echo ' cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe)'; \
+	    cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe);; \
+	esac;
+
+$(top_builddir)/config.status: $(top_srcdir)/configure $(CONFIG_STATUS_DEPENDENCIES)
+	cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
+
+$(top_srcdir)/configure:  $(am__configure_deps)
+	cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
+$(ACLOCAL_M4):  $(am__aclocal_m4_deps)
+	cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
+$(am__aclocal_m4_deps):
+
+mostlyclean-libtool:
+	-rm -f *.lo
+
+clean-libtool:
+	-rm -rf .libs _libs
+
+# This directory's subdirectories are mostly independent; you can cd
+# into them and run `make' without going through this Makefile.
+# To change the values of `make' variables: instead of editing Makefiles,
+# (1) if the variable is set in `config.status', edit `config.status'
+#     (which will cause the Makefiles to be regenerated when you run `make');
+# (2) otherwise, pass the desired values on the `make' command line.
+$(RECURSIVE_TARGETS):
+	@fail= failcom='exit 1'; \
+	for f in x $$MAKEFLAGS; do \
+	  case $$f in \
+	    *=* | --[!k]*);; \
+	    *k*) failcom='fail=yes';; \
+	  esac; \
+	done; \
+	dot_seen=no; \
+	target=`echo $@ | sed s/-recursive//`; \
+	list='$(SUBDIRS)'; for subdir in $$list; do \
+	  echo "Making $$target in $$subdir"; \
+	  if test "$$subdir" = "."; then \
+	    dot_seen=yes; \
+	    local_target="$$target-am"; \
+	  else \
+	    local_target="$$target"; \
+	  fi; \
+	  ($(am__cd) $$subdir && $(MAKE) $(AM_MAKEFLAGS) $$local_target) \
+	  || eval $$failcom; \
+	done; \
+	if test "$$dot_seen" = "no"; then \
+	  $(MAKE) $(AM_MAKEFLAGS) "$$target-am" || exit 1; \
+	fi; test -z "$$fail"
+
+$(RECURSIVE_CLEAN_TARGETS):
+	@fail= failcom='exit 1'; \
+	for f in x $$MAKEFLAGS; do \
+	  case $$f in \
+	    *=* | --[!k]*);; \
+	    *k*) failcom='fail=yes';; \
+	  esac; \
+	done; \
+	dot_seen=no; \
+	case "$@" in \
+	  distclean-* | maintainer-clean-*) list='$(DIST_SUBDIRS)' ;; \
+	  *) list='$(SUBDIRS)' ;; \
+	esac; \
+	rev=''; for subdir in $$list; do \
+	  if test "$$subdir" = "."; then :; else \
+	    rev="$$subdir $$rev"; \
+	  fi; \
+	done; \
+	rev="$$rev ."; \
+	target=`echo $@ | sed s/-recursive//`; \
+	for subdir in $$rev; do \
+	  echo "Making $$target in $$subdir"; \
+	  if test "$$subdir" = "."; then \
+	    local_target="$$target-am"; \
+	  else \
+	    local_target="$$target"; \
+	  fi; \
+	  ($(am__cd) $$subdir && $(MAKE) $(AM_MAKEFLAGS) $$local_target) \
+	  || eval $$failcom; \
+	done && test -z "$$fail"
+tags-recursive:
+	list='$(SUBDIRS)'; for subdir in $$list; do \
+	  test "$$subdir" = . || ($(am__cd) $$subdir && $(MAKE) $(AM_MAKEFLAGS) tags); \
+	done
+ctags-recursive:
+	list='$(SUBDIRS)'; for subdir in $$list; do \
+	  test "$$subdir" = . || ($(am__cd) $$subdir && $(MAKE) $(AM_MAKEFLAGS) ctags); \
+	done
+
+ID: $(HEADERS) $(SOURCES) $(LISP) $(TAGS_FILES)
+	list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \
+	unique=`for i in $$list; do \
+	    if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
+	  done | \
+	  $(AWK) '{ files[$$0] = 1; nonempty = 1; } \
+	      END { if (nonempty) { for (i in files) print i; }; }'`; \
+	mkid -fID $$unique
+tags: TAGS
+
+TAGS: tags-recursive $(HEADERS) $(SOURCES)  $(TAGS_DEPENDENCIES) \
+		$(TAGS_FILES) $(LISP)
+	set x; \
+	here=`pwd`; \
+	if ($(ETAGS) --etags-include --version) >/dev/null 2>&1; then \
+	  include_option=--etags-include; \
+	  empty_fix=.; \
+	else \
+	  include_option=--include; \
+	  empty_fix=; \
+	fi; \
+	list='$(SUBDIRS)'; for subdir in $$list; do \
+	  if test "$$subdir" = .; then :; else \
+	    test ! -f $$subdir/TAGS || \
+	      set "$$@" "$$include_option=$$here/$$subdir/TAGS"; \
+	  fi; \
+	done; \
+	list='$(SOURCES) $(HEADERS)  $(LISP) $(TAGS_FILES)'; \
+	unique=`for i in $$list; do \
+	    if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
+	  done | \
+	  $(AWK) '{ files[$$0] = 1; nonempty = 1; } \
+	      END { if (nonempty) { for (i in files) print i; }; }'`; \
+	shift; \
+	if test -z "$(ETAGS_ARGS)$$*$$unique"; then :; else \
+	  test -n "$$unique" || unique=$$empty_fix; \
+	  if test $$# -gt 0; then \
+	    $(ETAGS) $(ETAGSFLAGS) $(AM_ETAGSFLAGS) $(ETAGS_ARGS) \
+	      "$$@" $$unique; \
+	  else \
+	    $(ETAGS) $(ETAGSFLAGS) $(AM_ETAGSFLAGS) $(ETAGS_ARGS) \
+	      $$unique; \
+	  fi; \
+	fi
+ctags: CTAGS
+CTAGS: ctags-recursive $(HEADERS) $(SOURCES)  $(TAGS_DEPENDENCIES) \
+		$(TAGS_FILES) $(LISP)
+	list='$(SOURCES) $(HEADERS)  $(LISP) $(TAGS_FILES)'; \
+	unique=`for i in $$list; do \
+	    if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
+	  done | \
+	  $(AWK) '{ files[$$0] = 1; nonempty = 1; } \
+	      END { if (nonempty) { for (i in files) print i; }; }'`; \
+	test -z "$(CTAGS_ARGS)$$unique" \
+	  || $(CTAGS) $(CTAGSFLAGS) $(AM_CTAGSFLAGS) $(CTAGS_ARGS) \
+	     $$unique
+
+GTAGS:
+	here=`$(am__cd) $(top_builddir) && pwd` \
+	  && $(am__cd) $(top_srcdir) \
+	  && gtags -i $(GTAGS_ARGS) "$$here"
+
+distclean-tags:
+	-rm -f TAGS ID GTAGS GRTAGS GSYMS GPATH tags
+
+# To be appended to the command running the test.  Handle the stdout
+# and stderr redirection, and catch the exit status.
+am__check_post =					\
+>$@-t 2>&1;						\
+estatus=$$?;						\
+if test -n '$(DISABLE_HARD_ERRORS)'			\
+   && test $$estatus -eq 99; then			\
+  estatus=1;						\
+fi;							\
+TERM=$$__SAVED_TERM; export TERM;			\
+$(am__tty_colors);					\
+xfailed=PASS;						\
+case " $(XFAIL_TESTS) " in				\
+  *[\ \	]$$f[\ \	]* | *[\ \	]$$dir$$f[\ \	]*) \
+    xfailed=XFAIL;;					\
+esac;							\
+case $$estatus:$$xfailed in				\
+    0:XFAIL) col=$$red; res=XPASS;;			\
+    0:*)     col=$$grn; res=PASS ;;			\
+    77:*)    col=$$blu; res=SKIP ;;			\
+    99:*)    col=$$red; res=FAIL ;;			\
+    *:XFAIL) col=$$lgn; res=XFAIL;;			\
+    *:*)     col=$$red; res=FAIL ;;			\
+esac;							\
+echo "$${col}$$res$${std}: $$f";			\
+echo "$$res: $$f (exit: $$estatus)" |			\
+  $(am__rst_section) >$@;				\
+cat $@-t >>$@;						\
+rm -f $@-t
+
+$(TEST_SUITE_LOG): $(TEST_LOGS)
+	@$(am__sh_e_setup);						\
+	list='$(TEST_LOGS)';						\
+	results=`for f in $$list; do					\
+		   read line < $$f && echo "$$line" || echo FAIL;	\
+		 done`;							\
+	all=`echo "$$results" | sed '/^$$/d' | wc -l | sed -e 's/^[	 ]*//'`; \
+	fail=`echo "$$results" | grep -c '^FAIL'`;			\
+	pass=`echo "$$results" | grep -c '^PASS'`;			\
+	skip=`echo "$$results" | grep -c '^SKIP'`;			\
+	xfail=`echo "$$results" | grep -c '^XFAIL'`;			\
+	xpass=`echo "$$results" | grep -c '^XPASS'`;			\
+	failures=`expr $$fail + $$xpass`;				\
+	all=`expr $$all - $$skip`;					\
+	if test "$$all" -eq 1; then tests=test; All=;			\
+	else tests=tests; All="All "; fi;				\
+	case fail=$$fail:xpass=$$xpass:xfail=$$xfail in			\
+	  fail=0:xpass=0:xfail=0)					\
+	    msg="$$All$$all $$tests passed.  ";				\
+	    exit=true;;							\
+	  fail=0:xpass=0:xfail=*)					\
+	    msg="$$All$$all $$tests behaved as expected";		\
+	    if test "$$xfail" -eq 1; then xfailures=failure;		\
+	    else xfailures=failures; fi;				\
+	    msg="$$msg ($$xfail expected $$xfailures).  ";		\
+	    exit=true;;							\
+	  fail=*:xpass=0:xfail=*)					\
+	    msg="$$fail of $$all $$tests failed.  ";			\
+	    exit=false;;						\
+	  fail=*:xpass=*:xfail=*)					\
+	    msg="$$failures of $$all $$tests did not behave as expected"; \
+	    if test "$$xpass" -eq 1; then xpasses=pass;			\
+	    else xpasses=passes; fi;					\
+	    msg="$$msg ($$xpass unexpected $$xpasses).  ";		\
+	    exit=false;;						\
+	  *)								\
+	    echo >&2 "incorrect case"; exit 4;;				\
+	esac;								\
+	if test "$$skip" -ne 0; then					\
+	  if test "$$skip" -eq 1; then					\
+	    msg="$$msg($$skip test was not run).  ";			\
+	  else								\
+	    msg="$$msg($$skip tests were not run).  ";			\
+	  fi;								\
+	fi;								\
+	{								\
+	  echo "$(PACKAGE_STRING): $(subdir)/$(TEST_SUITE_LOG)" |	\
+	    $(am__rst_title);						\
+	  echo "$$msg";							\
+	  echo;								\
+	  echo ".. contents:: :depth: 2";				\
+	  echo;								\
+	  for f in $$list; do						\
+	    read line < $$f;						\
+	    case $$line in						\
+	      PASS:*|XFAIL:*);;						\
+	      *) echo; cat $$f;;					\
+	    esac;							\
+	  done;								\
+	} >$(TEST_SUITE_LOG).tmp;					\
+	mv $(TEST_SUITE_LOG).tmp $(TEST_SUITE_LOG);			\
+	if test "$$failures" -ne 0; then				\
+	  msg="$${msg}See $(subdir)/$(TEST_SUITE_LOG).  ";		\
+	  if test -n "$(PACKAGE_BUGREPORT)"; then			\
+	    msg="$${msg}Please report to $(PACKAGE_BUGREPORT).  ";	\
+	  fi;								\
+	fi;								\
+	test x"$$VERBOSE" = x || $$exit || cat $(TEST_SUITE_LOG);	\
+	$(am__tty_colors);						\
+	if $$exit; then							\
+	  echo $(ECHO_N) "$$grn$(ECHO_C)";				\
+	 else								\
+	  echo $(ECHO_N) "$$red$(ECHO_C)";				\
+	fi;								\
+	echo "$$msg" | $(am__text_box);					\
+	echo $(ECHO_N) "$$std$(ECHO_C)";				\
+	$$exit
+
+# Run all the tests.
+check-TESTS:
+	@list='$(RECHECK_LOGS)'; test -z "$$list" || rm -f $$list
+	@test -z "$(TEST_SUITE_LOG)" || rm -f $(TEST_SUITE_LOG)
+	@list='$(TEST_LOGS)';						\
+	list=`for f in $$list; do					\
+	  test .log = $$f || echo $$f;					\
+	done | tr '\012\015' '  '`;					\
+	$(MAKE) $(AM_MAKEFLAGS) $(TEST_SUITE_LOG) TEST_LOGS="$$list"
+
+.log.html:
+	@list='$(RST2HTML) $$RST2HTML rst2html rst2html.py';		\
+	for r2h in $$list; do						\
+	  if ($$r2h --version) >/dev/null 2>&1; then			\
+	    R2H=$$r2h;							\
+	  fi;								\
+	done;								\
+	if test -z "$$R2H"; then					\
+	  echo >&2 "cannot find rst2html, cannot create $@";		\
+	  exit 2;							\
+	fi;								\
+	$$R2H $< >$@.tmp
+	@mv $@.tmp $@
+
+# Be sure to run check first, and then to convert the result.
+# Beware of concurrent executions.  Run "check" not "check-TESTS", as
+# check-SCRIPTS and other dependencies are rebuilt by the former only.
+# And expect check to fail.
+check-html:
+	@if $(MAKE) $(AM_MAKEFLAGS) check; then			\
+	  rv=0; else rv=$$?;					\
+	fi;							\
+	$(MAKE) $(AM_MAKEFLAGS) $(TEST_SUITE_HTML) || exit 4;	\
+	exit $$rv
+recheck recheck-html:
+	@target=`echo $@ | sed 's,^re,,'`;				\
+	list='$(TEST_LOGS)';						\
+	list=`for f in $$list; do					\
+	        test -f $$f || continue;				\
+	        if read line < $$f; then				\
+	          case $$line in FAIL*|XPASS*) echo $$f;; esac;		\
+	        else echo $$f; fi;					\
+	      done | tr '\012\015' '  '`;				\
+	$(MAKE) $(AM_MAKEFLAGS) $$target AM_MAKEFLAGS='$(AM_MAKEFLAGS) TEST_LOGS="'"$$list"'"'
+.test.log:
+	@p='$<'; $(am__check_pre) $(TEST_LOG_COMPILE) "$$tst" $(am__check_post)
+@am__EXEEXT_TRUE@.test$(EXEEXT).log:
+@am__EXEEXT_TRUE@	@p='$<'; $(am__check_pre) $(TEST_LOG_COMPILE) "$$tst" $(am__check_post)
+
+distdir: $(DISTFILES)
+	@srcdirstrip=`echo "$(srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \
+	topsrcdirstrip=`echo "$(top_srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \
+	list='$(DISTFILES)'; \
+	  dist_files=`for file in $$list; do echo $$file; done | \
+	  sed -e "s|^$$srcdirstrip/||;t" \
+	      -e "s|^$$topsrcdirstrip/|$(top_builddir)/|;t"`; \
+	case $$dist_files in \
+	  */*) $(MKDIR_P) `echo "$$dist_files" | \
+			   sed '/\//!d;s|^|$(distdir)/|;s,/[^/]*$$,,' | \
+			   sort -u` ;; \
+	esac; \
+	for file in $$dist_files; do \
+	  if test -f $$file || test -d $$file; then d=.; else d=$(srcdir); fi; \
+	  if test -d $$d/$$file; then \
+	    dir=`echo "/$$file" | sed -e 's,/[^/]*$$,,'`; \
+	    if test -d "$(distdir)/$$file"; then \
+	      find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \
+	    fi; \
+	    if test -d $(srcdir)/$$file && test $$d != $(srcdir); then \
+	      cp -fpR $(srcdir)/$$file "$(distdir)$$dir" || exit 1; \
+	      find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \
+	    fi; \
+	    cp -fpR $$d/$$file "$(distdir)$$dir" || exit 1; \
+	  else \
+	    test -f "$(distdir)/$$file" \
+	    || cp -p $$d/$$file "$(distdir)/$$file" \
+	    || exit 1; \
+	  fi; \
+	done
+	@list='$(DIST_SUBDIRS)'; for subdir in $$list; do \
+	  if test "$$subdir" = .; then :; else \
+	    test -d "$(distdir)/$$subdir" \
+	    || $(MKDIR_P) "$(distdir)/$$subdir" \
+	    || exit 1; \
+	  fi; \
+	done
+	@list='$(DIST_SUBDIRS)'; for subdir in $$list; do \
+	  if test "$$subdir" = .; then :; else \
+	    dir1=$$subdir; dir2="$(distdir)/$$subdir"; \
+	    $(am__relativize); \
+	    new_distdir=$$reldir; \
+	    dir1=$$subdir; dir2="$(top_distdir)"; \
+	    $(am__relativize); \
+	    new_top_distdir=$$reldir; \
+	    echo " (cd $$subdir && $(MAKE) $(AM_MAKEFLAGS) top_distdir="$$new_top_distdir" distdir="$$new_distdir" \\"; \
+	    echo "     am__remove_distdir=: am__skip_length_check=: am__skip_mode_fix=: distdir)"; \
+	    ($(am__cd) $$subdir && \
+	      $(MAKE) $(AM_MAKEFLAGS) \
+	        top_distdir="$$new_top_distdir" \
+	        distdir="$$new_distdir" \
+		am__remove_distdir=: \
+		am__skip_length_check=: \
+		am__skip_mode_fix=: \
+	        distdir) \
+	      || exit 1; \
+	  fi; \
+	done
+check-am: all-am
+	$(MAKE) $(AM_MAKEFLAGS) check-TESTS
+check: check-recursive
+all-am: Makefile
+installdirs: installdirs-recursive
+installdirs-am:
+install: install-recursive
+install-exec: install-exec-recursive
+install-data: install-data-recursive
+uninstall: uninstall-recursive
+
+install-am: all-am
+	@$(MAKE) $(AM_MAKEFLAGS) install-exec-am install-data-am
+
+installcheck: installcheck-recursive
+install-strip:
+	$(MAKE) $(AM_MAKEFLAGS) INSTALL_PROGRAM="$(INSTALL_STRIP_PROGRAM)" \
+	  install_sh_PROGRAM="$(INSTALL_STRIP_PROGRAM)" INSTALL_STRIP_FLAG=-s \
+	  `test -z '$(STRIP)' || \
+	    echo "INSTALL_PROGRAM_ENV=STRIPPROG='$(STRIP)'"` install
+mostlyclean-generic:
+	-test -z "$(TEST_LOGS)" || rm -f $(TEST_LOGS)
+	-test -z "$(TEST_LOGS_TMP)" || rm -f $(TEST_LOGS_TMP)
+	-test -z "$(TEST_SUITE_HTML)" || rm -f $(TEST_SUITE_HTML)
+	-test -z "$(TEST_SUITE_LOG)" || rm -f $(TEST_SUITE_LOG)
+
+clean-generic:
+
+distclean-generic:
+	-test -z "$(CONFIG_CLEAN_FILES)" || rm -f $(CONFIG_CLEAN_FILES)
+	-test . = "$(srcdir)" || test -z "$(CONFIG_CLEAN_VPATH_FILES)" || rm -f $(CONFIG_CLEAN_VPATH_FILES)
+
+maintainer-clean-generic:
+	@echo "This command is intended for maintainers to use"
+	@echo "it deletes files that may require special tools to rebuild."
+clean: clean-recursive
+
+clean-am: clean-generic clean-libtool mostlyclean-am
+
+distclean: distclean-recursive
+	-rm -f Makefile
+distclean-am: clean-am distclean-generic distclean-tags
+
+dvi: dvi-recursive
+
+dvi-am:
+
+html: html-recursive
+
+html-am:
+
+info: info-recursive
+
+info-am:
+
+install-data-am:
+
+install-dvi: install-dvi-recursive
+
+install-dvi-am:
+
+install-exec-am:
+
+install-html: install-html-recursive
+
+install-html-am:
+
+install-info: install-info-recursive
+
+install-info-am:
+
+install-man:
+
+install-pdf: install-pdf-recursive
+
+install-pdf-am:
+
+install-ps: install-ps-recursive
+
+install-ps-am:
+
+installcheck-am:
+
+maintainer-clean: maintainer-clean-recursive
+	-rm -f Makefile
+maintainer-clean-am: distclean-am maintainer-clean-generic
+
+mostlyclean: mostlyclean-recursive
+
+mostlyclean-am: mostlyclean-generic mostlyclean-libtool
+
+pdf: pdf-recursive
+
+pdf-am:
+
+ps: ps-recursive
+
+ps-am:
+
+uninstall-am:
+
+.MAKE: $(RECURSIVE_CLEAN_TARGETS) $(RECURSIVE_TARGETS) check-am \
+	check-html ctags-recursive install-am install-strip recheck \
+	recheck-html tags-recursive
+
+.PHONY: $(RECURSIVE_CLEAN_TARGETS) $(RECURSIVE_TARGETS) CTAGS GTAGS \
+	all all-am check check-TESTS check-am check-html clean \
+	clean-generic clean-libtool ctags ctags-recursive distclean \
+	distclean-generic distclean-libtool distclean-tags distdir dvi \
+	dvi-am html html-am info info-am install install-am \
+	install-data install-data-am install-dvi install-dvi-am \
+	install-exec install-exec-am install-html install-html-am \
+	install-info install-info-am install-man install-pdf \
+	install-pdf-am install-ps install-ps-am install-strip \
+	installcheck installcheck-am installdirs installdirs-am \
+	maintainer-clean maintainer-clean-generic mostlyclean \
+	mostlyclean-generic mostlyclean-libtool pdf pdf-am ps ps-am \
+	recheck recheck-html tags tags-recursive uninstall \
+	uninstall-am
+
+
+# Tell versions [3.59,3.63) of GNU make to not export all variables.
+# Otherwise a system limit (for SysV at least) may be exceeded.
+.NOEXPORT:
diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am
new file mode 100644
index 000000000..0624c00f1
--- /dev/null
+++ b/test/regress/regress0/bv/core/Makefile.am
@@ -0,0 +1,50 @@
+TESTS_ENVIRONMENT = @srcdir@/../../../run_regression @top_builddir@/src/main/cvc4
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS =	\
+	concat-merge-0.smt \ 
+	concat-merge-1.smt \ 
+	concat-merge-2.smt \ 
+	concat-merge-3.smt \ 
+	extract-concat-0.smt \ 
+	extract-concat-1.smt \ 
+	extract-concat-2.smt \ 
+	extract-concat-3.smt \ 
+	extract-concat-4.smt \ 
+	extract-concat-5.smt \ 
+	extract-concat-6.smt \ 
+	extract-concat-7.smt \ 
+	extract-concat-8.smt \ 
+	extract-concat-9.smt \ 
+	extract-concat-10.smt \ 
+	extract-concat-11.smt \ 
+	extract-constant.smt \ 
+	extract-extract-0.smt \ 
+	extract-extract-1.smt \ 
+	extract-extract-2.smt \ 
+	extract-extract-3.smt \ 
+	extract-extract-4.smt \ 
+	extract-extract-5.smt \ 
+	extract-extract-6.smt \ 
+	extract-extract-7.smt \ 
+	extract-extract-8.smt \ 
+	extract-extract-9.smt \ 
+	extract-extract-10.smt \ 
+	extract-extract-11.smt \ 
+	extract-whole-0.smt \ 
+	extract-whole-1.smt \ 
+	extract-whole-2.smt \ 
+	extract-whole-3.smt \ 
+	extract-whole-4.smt  
+
+EXTRA_DIST = $(TESTS)
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:
diff --git a/test/regress/regress0/bv/core/Makefile.in b/test/regress/regress0/bv/core/Makefile.in
new file mode 100644
index 000000000..564ed19ba
--- /dev/null
+++ b/test/regress/regress0/bv/core/Makefile.in
@@ -0,0 +1,788 @@
+# Makefile.in generated by automake 1.11.1 from Makefile.am.
+# @configure_input@
+
+# Copyright (C) 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001, 2002,
+# 2003, 2004, 2005, 2006, 2007, 2008, 2009  Free Software Foundation,
+# Inc.
+# This Makefile.in is free software; the Free Software Foundation
+# gives unlimited permission to copy and/or distribute it,
+# with or without modifications, as long as this notice is preserved.
+
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY, to the extent permitted by law; without
+# even the implied warranty of MERCHANTABILITY or FITNESS FOR A
+# PARTICULAR PURPOSE.
+
+@SET_MAKE@
+VPATH = @srcdir@
+pkgdatadir = $(datadir)/@PACKAGE@
+pkgincludedir = $(includedir)/@PACKAGE@
+pkglibdir = $(libdir)/@PACKAGE@
+pkglibexecdir = $(libexecdir)/@PACKAGE@
+am__cd = CDPATH="$${ZSH_VERSION+.}$(PATH_SEPARATOR)" && cd
+install_sh_DATA = $(install_sh) -c -m 644
+install_sh_PROGRAM = $(install_sh) -c
+install_sh_SCRIPT = $(install_sh) -c
+INSTALL_HEADER = $(INSTALL_DATA)
+transform = $(program_transform_name)
+NORMAL_INSTALL = :
+PRE_INSTALL = :
+POST_INSTALL = :
+NORMAL_UNINSTALL = :
+PRE_UNINSTALL = :
+POST_UNINSTALL = :
+build_triplet = @build@
+host_triplet = @host@
+target_triplet = @target@
+subdir = test/regress/regress0/bv/core
+DIST_COMMON = $(srcdir)/Makefile.am $(srcdir)/Makefile.in
+ACLOCAL_M4 = $(top_srcdir)/aclocal.m4
+am__aclocal_m4_deps = $(top_srcdir)/config/antlr.m4 \
+	$(top_srcdir)/config/ax_prog_doxygen.m4 \
+	$(top_srcdir)/config/cvc4.m4 $(top_srcdir)/config/libtool.m4 \
+	$(top_srcdir)/config/ltoptions.m4 \
+	$(top_srcdir)/config/ltsugar.m4 \
+	$(top_srcdir)/config/ltversion.m4 \
+	$(top_srcdir)/config/lt~obsolete.m4 \
+	$(top_srcdir)/config/pkg.m4 $(top_srcdir)/configure.ac
+am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \
+	$(ACLOCAL_M4)
+mkinstalldirs = $(install_sh) -d
+CONFIG_HEADER = $(top_builddir)/cvc4autoconfig.h
+CONFIG_CLEAN_FILES =
+CONFIG_CLEAN_VPATH_FILES =
+AM_V_GEN = $(am__v_GEN_$(V))
+am__v_GEN_ = $(am__v_GEN_$(AM_DEFAULT_VERBOSITY))
+am__v_GEN_0 = @echo "  GEN   " $@;
+AM_V_at = $(am__v_at_$(V))
+am__v_at_ = $(am__v_at_$(AM_DEFAULT_VERBOSITY))
+am__v_at_0 = @
+SOURCES =
+DIST_SOURCES =
+# If stdout is a non-dumb tty, use colors.  If test -t is not supported,
+# then this fails; a conservative approach.  Of course do not redirect
+# stdout here, just stderr.
+am__tty_colors = \
+red=; grn=; lgn=; blu=; std=; \
+test "X$(AM_COLOR_TESTS)" != Xno \
+&& test "X$$TERM" != Xdumb \
+&& { test "X$(AM_COLOR_TESTS)" = Xalways || test -t 1 2>/dev/null; } \
+&& { \
+  red=''; \
+  grn=''; \
+  lgn=''; \
+  blu=''; \
+  std=''; \
+}
+am__vpath_adj_setup = srcdirstrip=`echo "$(srcdir)" | sed 's|.|.|g'`;
+am__vpath_adj = case $$p in \
+    $(srcdir)/*) f=`echo "$$p" | sed "s|^$$srcdirstrip/||"`;; \
+    *) f=$$p;; \
+  esac;
+am__strip_dir = f=`echo $$p | sed -e 's|^.*/||'`;
+am__install_max = 40
+am__nobase_strip_setup = \
+  srcdirstrip=`echo "$(srcdir)" | sed 's/[].[^$$\\*|]/\\\\&/g'`
+am__nobase_strip = \
+  for p in $$list; do echo "$$p"; done | sed -e "s|$$srcdirstrip/||"
+am__nobase_list = $(am__nobase_strip_setup); \
+  for p in $$list; do echo "$$p $$p"; done | \
+  sed "s| $$srcdirstrip/| |;"' / .*\//!s/ .*/ ./; s,\( .*\)/[^/]*$$,\1,' | \
+  $(AWK) 'BEGIN { files["."] = "" } { files[$$2] = files[$$2] " " $$1; \
+    if (++n[$$2] == $(am__install_max)) \
+      { print $$2, files[$$2]; n[$$2] = 0; files[$$2] = "" } } \
+    END { for (dir in files) print dir, files[dir] }'
+am__base_list = \
+  sed '$$!N;$$!N;$$!N;$$!N;$$!N;$$!N;$$!N;s/\n/ /g' | \
+  sed '$$!N;$$!N;$$!N;$$!N;s/\n/ /g'
+# Restructured Text title and section.
+am__rst_title = sed 's/.*/   &   /;h;s/./=/g;p;x;p;g;p;s/.*//'
+am__rst_section = sed 'p;s/./=/g;p;g'
+# Put stdin (possibly several lines separated by ".  ") in a box.
+am__text_box = $(AWK) '{				\
+  n = split($$0, lines, "\\.  "); max = 0;		\
+  for (i = 1; i <= n; ++i)				\
+    if (max < length(lines[i]))				\
+      max = length(lines[i]);				\
+  for (i = 0; i < max; ++i) line = line "=";		\
+  print line;						\
+  for (i = 1; i <= n; ++i) if (lines[i]) print lines[i];\
+  print line;						\
+}'
+# Solaris 10 'make', and several other traditional 'make' implementations,
+# pass "-e" to $(SHELL).  This contradicts POSIX.  Work around the problem
+# by disabling -e (using the XSI extension "set +e") if it's set.
+am__sh_e_setup = case $$- in *e*) set +e;; esac
+# To be inserted before the command running the test.  Creates the
+# directory for the log if needed.  Stores in $dir the directory
+# containing $f, in $tst the test, in $log the log, and passes
+# TESTS_ENVIRONMENT.  Save and restore TERM around use of
+# TESTS_ENVIRONMENT, in case that unsets it.
+am__check_pre = \
+$(am__sh_e_setup);					\
+$(am__vpath_adj_setup) $(am__vpath_adj)			\
+srcdir=$(srcdir); export srcdir;			\
+rm -f $@-t;						\
+trap 'st=$$?; rm -f '\''$(abs_builddir)/$@-t'\''; (exit $$st); exit $$st' \
+  1 2 13 15;						\
+am__odir=`echo "./$@" | sed 's|/[^/]*$$||'`;		\
+test "x$$am__odir" = x. || $(MKDIR_P) "$$am__odir" || exit $$?;	\
+if test -f "./$$f"; then dir=./;			\
+elif test -f "$$f"; then dir=;				\
+else dir="$(srcdir)/"; fi;				\
+tst=$$dir$$f; log='$@'; __SAVED_TERM=$$TERM;		\
+$(TESTS_ENVIRONMENT)
+RECHECK_LOGS = $(TEST_LOGS)
+AM_RECURSIVE_TARGETS = check check-html recheck recheck-html
+TEST_SUITE_LOG = test-suite.log
+TEST_SUITE_HTML = $(TEST_SUITE_LOG:.log=.html)
+TEST_EXTENSIONS = @EXEEXT@ .test
+LOG_COMPILE = $(LOG_COMPILER) $(AM_LOG_FLAGS) $(LOG_FLAGS)
+am__test_logs1 = $(TESTS:=.log)
+am__test_logs2 = $(am__test_logs1:@EXEEXT@.log=.log)
+TEST_LOGS = $(am__test_logs2:.test.log=.log)
+TEST_LOG_COMPILE = $(TEST_LOG_COMPILER) $(AM_TEST_LOG_FLAGS) \
+	$(TEST_LOG_FLAGS)
+TEST_LOGS_TMP = $(TEST_LOGS:.log=.log-t)
+DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST)
+ACLOCAL = @ACLOCAL@
+AMTAR = @AMTAR@
+AM_DEFAULT_VERBOSITY = @AM_DEFAULT_VERBOSITY@
+ANTLR = @ANTLR@
+ANTLR_HOME = @ANTLR_HOME@
+ANTLR_INCLUDES = @ANTLR_INCLUDES@
+ANTLR_LDFLAGS = @ANTLR_LDFLAGS@
+AR = @AR@
+AS = @AS@
+AUTOCONF = @AUTOCONF@
+AUTOHEADER = @AUTOHEADER@
+AUTOMAKE = @AUTOMAKE@
+AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
+CC = @CC@
+CCDEPMODE = @CCDEPMODE@
+CFLAGS = @CFLAGS@
+CLN_CFLAGS = @CLN_CFLAGS@
+CLN_LIBS = @CLN_LIBS@
+CPP = @CPP@
+CPPFLAGS = @CPPFLAGS@
+CVC4_LIBRARY_VERSION = @CVC4_LIBRARY_VERSION@
+CVC4_PARSER_LIBRARY_VERSION = @CVC4_PARSER_LIBRARY_VERSION@
+CVC4_USE_CLN_IMP = @CVC4_USE_CLN_IMP@
+CVC4_USE_GMP_IMP = @CVC4_USE_GMP_IMP@
+CXX = @CXX@
+CXXCPP = @CXXCPP@
+CXXDEPMODE = @CXXDEPMODE@
+CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
+CXXTESTGEN = @CXXTESTGEN@
+CYGPATH_W = @CYGPATH_W@
+DEFS = @DEFS@
+DEPDIR = @DEPDIR@
+DLLTOOL = @DLLTOOL@
+DOXYGEN_PAPER_SIZE = @DOXYGEN_PAPER_SIZE@
+DSYMUTIL = @DSYMUTIL@
+DUMPBIN = @DUMPBIN@
+DX_CONFIG = @DX_CONFIG@
+DX_DOCDIR = @DX_DOCDIR@
+DX_DOT = @DX_DOT@
+DX_DOXYGEN = @DX_DOXYGEN@
+DX_DVIPS = @DX_DVIPS@
+DX_EGREP = @DX_EGREP@
+DX_ENV = @DX_ENV@
+DX_FLAG_DX_CURRENT_FEATURE = @DX_FLAG_DX_CURRENT_FEATURE@
+DX_FLAG_chi = @DX_FLAG_chi@
+DX_FLAG_chm = @DX_FLAG_chm@
+DX_FLAG_doc = @DX_FLAG_doc@
+DX_FLAG_dot = @DX_FLAG_dot@
+DX_FLAG_html = @DX_FLAG_html@
+DX_FLAG_man = @DX_FLAG_man@
+DX_FLAG_pdf = @DX_FLAG_pdf@
+DX_FLAG_ps = @DX_FLAG_ps@
+DX_FLAG_rtf = @DX_FLAG_rtf@
+DX_FLAG_xml = @DX_FLAG_xml@
+DX_HHC = @DX_HHC@
+DX_LATEX = @DX_LATEX@
+DX_MAKEINDEX = @DX_MAKEINDEX@
+DX_PDFLATEX = @DX_PDFLATEX@
+DX_PERL = @DX_PERL@
+DX_PROJECT = @DX_PROJECT@
+ECHO_C = @ECHO_C@
+ECHO_N = @ECHO_N@
+ECHO_T = @ECHO_T@
+EGREP = @EGREP@
+EXEEXT = @EXEEXT@
+FGREP = @FGREP@
+FLAG_VISIBILITY_HIDDEN = @FLAG_VISIBILITY_HIDDEN@
+GREP = @GREP@
+INSTALL = @INSTALL@
+INSTALL_DATA = @INSTALL_DATA@
+INSTALL_PROGRAM = @INSTALL_PROGRAM@
+INSTALL_SCRIPT = @INSTALL_SCRIPT@
+INSTALL_STRIP_PROGRAM = @INSTALL_STRIP_PROGRAM@
+LD = @LD@
+LDFLAGS = @LDFLAGS@
+LIBOBJS = @LIBOBJS@
+LIBS = @LIBS@
+LIBTOOL = @LIBTOOL@
+LIPO = @LIPO@
+LN_S = @LN_S@
+LTLIBOBJS = @LTLIBOBJS@
+MAKEINFO = @MAKEINFO@
+MKDIR_P = @MKDIR_P@
+NM = @NM@
+NMEDIT = @NMEDIT@
+OBJDUMP = @OBJDUMP@
+OBJEXT = @OBJEXT@
+OTOOL = @OTOOL@
+OTOOL64 = @OTOOL64@
+PACKAGE = @PACKAGE@
+PACKAGE_BUGREPORT = @PACKAGE_BUGREPORT@
+PACKAGE_NAME = @PACKAGE_NAME@
+PACKAGE_STRING = @PACKAGE_STRING@
+PACKAGE_TARNAME = @PACKAGE_TARNAME@
+PACKAGE_URL = @PACKAGE_URL@
+PACKAGE_VERSION = @PACKAGE_VERSION@
+PATH_SEPARATOR = @PATH_SEPARATOR@
+PERL = @PERL@
+PKG_CONFIG = @PKG_CONFIG@
+RANLIB = @RANLIB@
+SED = @SED@
+SET_MAKE = @SET_MAKE@
+SHELL = @SHELL@
+STATIC_BINARY = @STATIC_BINARY@
+STRIP = @STRIP@
+TEST_CPPFLAGS = @TEST_CPPFLAGS@
+TEST_CXXFLAGS = @TEST_CXXFLAGS@
+TEST_LDFLAGS = @TEST_LDFLAGS@
+VERSION = @VERSION@
+abs_builddir = @abs_builddir@
+abs_srcdir = @abs_srcdir@
+abs_top_builddir = @abs_top_builddir@
+abs_top_srcdir = @abs_top_srcdir@
+ac_ct_CC = @ac_ct_CC@
+ac_ct_CXX = @ac_ct_CXX@
+ac_ct_DUMPBIN = @ac_ct_DUMPBIN@
+am__include = @am__include@
+am__leading_dot = @am__leading_dot@
+am__quote = @am__quote@
+am__tar = @am__tar@
+am__untar = @am__untar@
+bindir = @bindir@
+build = @build@
+build_alias = @build_alias@
+build_cpu = @build_cpu@
+build_os = @build_os@
+build_vendor = @build_vendor@
+builddir = @builddir@
+datadir = @datadir@
+datarootdir = @datarootdir@
+docdir = @docdir@
+dvidir = @dvidir@
+exec_prefix = @exec_prefix@
+host = @host@
+host_alias = @host_alias@
+host_cpu = @host_cpu@
+host_os = @host_os@
+host_vendor = @host_vendor@
+htmldir = @htmldir@
+includedir = @includedir@
+infodir = @infodir@
+install_sh = @install_sh@
+libdir = @libdir@
+libexecdir = @libexecdir@
+localedir = @localedir@
+localstatedir = @localstatedir@
+lt_ECHO = @lt_ECHO@
+mandir = @mandir@
+mk_include = @mk_include@
+mkdir_p = @mkdir_p@
+oldincludedir = @oldincludedir@
+pdfdir = @pdfdir@
+prefix = @prefix@
+program_transform_name = @program_transform_name@
+psdir = @psdir@
+sbindir = @sbindir@
+sharedstatedir = @sharedstatedir@
+srcdir = @srcdir@
+sysconfdir = @sysconfdir@
+target = @target@
+target_alias = @target_alias@
+target_cpu = @target_cpu@
+target_os = @target_os@
+target_vendor = @target_vendor@
+top_build_prefix = @top_build_prefix@
+top_builddir = @top_builddir@
+top_srcdir = @top_srcdir@
+TESTS_ENVIRONMENT = @srcdir@/../../../run_regression @top_builddir@/src/main/cvc4
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS = \
+	concat-merge-0.smt \
+	concat-merge-1.smt \
+	concat-merge-2.smt \
+	concat-merge-3.smt \
+	extract-concat-0.smt \
+	extract-concat-1.smt \
+	extract-concat-2.smt \
+	extract-concat-3.smt \
+	extract-concat-4.smt \
+	extract-concat-5.smt \
+	extract-concat-6.smt \
+	extract-concat-7.smt \
+	extract-concat-8.smt \
+	extract-concat-9.smt \
+	extract-concat-10.smt \
+	extract-concat-11.smt \
+	extract-constant.smt \
+	extract-extract-0.smt \
+	extract-extract-1.smt \
+	extract-extract-2.smt \
+	extract-extract-3.smt \
+	extract-extract-4.smt \
+	extract-extract-5.smt \
+	extract-extract-6.smt \
+	extract-extract-7.smt \
+	extract-extract-8.smt \
+	extract-extract-9.smt \
+	extract-extract-10.smt \
+	extract-extract-11.smt \
+	extract-whole-0.smt \
+	extract-whole-1.smt \
+	extract-whole-2.smt \
+	extract-whole-3.smt \
+	extract-whole-4.smt  
+
+EXTRA_DIST = $(TESTS)
+all: all-am
+
+.SUFFIXES:
+.SUFFIXES: .html .log .test .test$(EXEEXT)
+$(srcdir)/Makefile.in:  $(srcdir)/Makefile.am  $(am__configure_deps)
+	@for dep in $?; do \
+	  case '$(am__configure_deps)' in \
+	    *$$dep*) \
+	      ( cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh ) \
+	        && { if test -f $@; then exit 0; else break; fi; }; \
+	      exit 1;; \
+	  esac; \
+	done; \
+	echo ' cd $(top_srcdir) && $(AUTOMAKE) --gnu test/regress/regress0/bv/core/Makefile'; \
+	$(am__cd) $(top_srcdir) && \
+	  $(AUTOMAKE) --gnu test/regress/regress0/bv/core/Makefile
+.PRECIOUS: Makefile
+Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status
+	@case '$?' in \
+	  *config.status*) \
+	    cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh;; \
+	  *) \
+	    echo ' cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe)'; \
+	    cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe);; \
+	esac;
+
+$(top_builddir)/config.status: $(top_srcdir)/configure $(CONFIG_STATUS_DEPENDENCIES)
+	cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
+
+$(top_srcdir)/configure:  $(am__configure_deps)
+	cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
+$(ACLOCAL_M4):  $(am__aclocal_m4_deps)
+	cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
+$(am__aclocal_m4_deps):
+
+mostlyclean-libtool:
+	-rm -f *.lo
+
+clean-libtool:
+	-rm -rf .libs _libs
+tags: TAGS
+TAGS:
+
+ctags: CTAGS
+CTAGS:
+
+
+# To be appended to the command running the test.  Handle the stdout
+# and stderr redirection, and catch the exit status.
+am__check_post =					\
+>$@-t 2>&1;						\
+estatus=$$?;						\
+if test -n '$(DISABLE_HARD_ERRORS)'			\
+   && test $$estatus -eq 99; then			\
+  estatus=1;						\
+fi;							\
+TERM=$$__SAVED_TERM; export TERM;			\
+$(am__tty_colors);					\
+xfailed=PASS;						\
+case " $(XFAIL_TESTS) " in				\
+  *[\ \	]$$f[\ \	]* | *[\ \	]$$dir$$f[\ \	]*) \
+    xfailed=XFAIL;;					\
+esac;							\
+case $$estatus:$$xfailed in				\
+    0:XFAIL) col=$$red; res=XPASS;;			\
+    0:*)     col=$$grn; res=PASS ;;			\
+    77:*)    col=$$blu; res=SKIP ;;			\
+    99:*)    col=$$red; res=FAIL ;;			\
+    *:XFAIL) col=$$lgn; res=XFAIL;;			\
+    *:*)     col=$$red; res=FAIL ;;			\
+esac;							\
+echo "$${col}$$res$${std}: $$f";			\
+echo "$$res: $$f (exit: $$estatus)" |			\
+  $(am__rst_section) >$@;				\
+cat $@-t >>$@;						\
+rm -f $@-t
+
+$(TEST_SUITE_LOG): $(TEST_LOGS)
+	@$(am__sh_e_setup);						\
+	list='$(TEST_LOGS)';						\
+	results=`for f in $$list; do					\
+		   read line < $$f && echo "$$line" || echo FAIL;	\
+		 done`;							\
+	all=`echo "$$results" | sed '/^$$/d' | wc -l | sed -e 's/^[	 ]*//'`; \
+	fail=`echo "$$results" | grep -c '^FAIL'`;			\
+	pass=`echo "$$results" | grep -c '^PASS'`;			\
+	skip=`echo "$$results" | grep -c '^SKIP'`;			\
+	xfail=`echo "$$results" | grep -c '^XFAIL'`;			\
+	xpass=`echo "$$results" | grep -c '^XPASS'`;			\
+	failures=`expr $$fail + $$xpass`;				\
+	all=`expr $$all - $$skip`;					\
+	if test "$$all" -eq 1; then tests=test; All=;			\
+	else tests=tests; All="All "; fi;				\
+	case fail=$$fail:xpass=$$xpass:xfail=$$xfail in			\
+	  fail=0:xpass=0:xfail=0)					\
+	    msg="$$All$$all $$tests passed.  ";				\
+	    exit=true;;							\
+	  fail=0:xpass=0:xfail=*)					\
+	    msg="$$All$$all $$tests behaved as expected";		\
+	    if test "$$xfail" -eq 1; then xfailures=failure;		\
+	    else xfailures=failures; fi;				\
+	    msg="$$msg ($$xfail expected $$xfailures).  ";		\
+	    exit=true;;							\
+	  fail=*:xpass=0:xfail=*)					\
+	    msg="$$fail of $$all $$tests failed.  ";			\
+	    exit=false;;						\
+	  fail=*:xpass=*:xfail=*)					\
+	    msg="$$failures of $$all $$tests did not behave as expected"; \
+	    if test "$$xpass" -eq 1; then xpasses=pass;			\
+	    else xpasses=passes; fi;					\
+	    msg="$$msg ($$xpass unexpected $$xpasses).  ";		\
+	    exit=false;;						\
+	  *)								\
+	    echo >&2 "incorrect case"; exit 4;;				\
+	esac;								\
+	if test "$$skip" -ne 0; then					\
+	  if test "$$skip" -eq 1; then					\
+	    msg="$$msg($$skip test was not run).  ";			\
+	  else								\
+	    msg="$$msg($$skip tests were not run).  ";			\
+	  fi;								\
+	fi;								\
+	{								\
+	  echo "$(PACKAGE_STRING): $(subdir)/$(TEST_SUITE_LOG)" |	\
+	    $(am__rst_title);						\
+	  echo "$$msg";							\
+	  echo;								\
+	  echo ".. contents:: :depth: 2";				\
+	  echo;								\
+	  for f in $$list; do						\
+	    read line < $$f;						\
+	    case $$line in						\
+	      PASS:*|XFAIL:*);;						\
+	      *) echo; cat $$f;;					\
+	    esac;							\
+	  done;								\
+	} >$(TEST_SUITE_LOG).tmp;					\
+	mv $(TEST_SUITE_LOG).tmp $(TEST_SUITE_LOG);			\
+	if test "$$failures" -ne 0; then				\
+	  msg="$${msg}See $(subdir)/$(TEST_SUITE_LOG).  ";		\
+	  if test -n "$(PACKAGE_BUGREPORT)"; then			\
+	    msg="$${msg}Please report to $(PACKAGE_BUGREPORT).  ";	\
+	  fi;								\
+	fi;								\
+	test x"$$VERBOSE" = x || $$exit || cat $(TEST_SUITE_LOG);	\
+	$(am__tty_colors);						\
+	if $$exit; then							\
+	  echo $(ECHO_N) "$$grn$(ECHO_C)";				\
+	 else								\
+	  echo $(ECHO_N) "$$red$(ECHO_C)";				\
+	fi;								\
+	echo "$$msg" | $(am__text_box);					\
+	echo $(ECHO_N) "$$std$(ECHO_C)";				\
+	$$exit
+
+# Run all the tests.
+check-TESTS:
+	@list='$(RECHECK_LOGS)'; test -z "$$list" || rm -f $$list
+	@test -z "$(TEST_SUITE_LOG)" || rm -f $(TEST_SUITE_LOG)
+	@list='$(TEST_LOGS)';						\
+	list=`for f in $$list; do					\
+	  test .log = $$f || echo $$f;					\
+	done | tr '\012\015' '  '`;					\
+	$(MAKE) $(AM_MAKEFLAGS) $(TEST_SUITE_LOG) TEST_LOGS="$$list"
+
+.log.html:
+	@list='$(RST2HTML) $$RST2HTML rst2html rst2html.py';		\
+	for r2h in $$list; do						\
+	  if ($$r2h --version) >/dev/null 2>&1; then			\
+	    R2H=$$r2h;							\
+	  fi;								\
+	done;								\
+	if test -z "$$R2H"; then					\
+	  echo >&2 "cannot find rst2html, cannot create $@";		\
+	  exit 2;							\
+	fi;								\
+	$$R2H $< >$@.tmp
+	@mv $@.tmp $@
+
+# Be sure to run check first, and then to convert the result.
+# Beware of concurrent executions.  Run "check" not "check-TESTS", as
+# check-SCRIPTS and other dependencies are rebuilt by the former only.
+# And expect check to fail.
+check-html:
+	@if $(MAKE) $(AM_MAKEFLAGS) check; then			\
+	  rv=0; else rv=$$?;					\
+	fi;							\
+	$(MAKE) $(AM_MAKEFLAGS) $(TEST_SUITE_HTML) || exit 4;	\
+	exit $$rv
+recheck recheck-html:
+	@target=`echo $@ | sed 's,^re,,'`;				\
+	list='$(TEST_LOGS)';						\
+	list=`for f in $$list; do					\
+	        test -f $$f || continue;				\
+	        if read line < $$f; then				\
+	          case $$line in FAIL*|XPASS*) echo $$f;; esac;		\
+	        else echo $$f; fi;					\
+	      done | tr '\012\015' '  '`;				\
+	$(MAKE) $(AM_MAKEFLAGS) $$target AM_MAKEFLAGS='$(AM_MAKEFLAGS) TEST_LOGS="'"$$list"'"'
+concat-merge-0.smt.log: concat-merge-0.smt
+	@p='concat-merge-0.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+concat-merge-1.smt.log: concat-merge-1.smt
+	@p='concat-merge-1.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+concat-merge-2.smt.log: concat-merge-2.smt
+	@p='concat-merge-2.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+concat-merge-3.smt.log: concat-merge-3.smt
+	@p='concat-merge-3.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-concat-0.smt.log: extract-concat-0.smt
+	@p='extract-concat-0.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-concat-1.smt.log: extract-concat-1.smt
+	@p='extract-concat-1.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-concat-2.smt.log: extract-concat-2.smt
+	@p='extract-concat-2.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-concat-3.smt.log: extract-concat-3.smt
+	@p='extract-concat-3.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-concat-4.smt.log: extract-concat-4.smt
+	@p='extract-concat-4.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-concat-5.smt.log: extract-concat-5.smt
+	@p='extract-concat-5.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-concat-6.smt.log: extract-concat-6.smt
+	@p='extract-concat-6.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-concat-7.smt.log: extract-concat-7.smt
+	@p='extract-concat-7.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-concat-8.smt.log: extract-concat-8.smt
+	@p='extract-concat-8.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-concat-9.smt.log: extract-concat-9.smt
+	@p='extract-concat-9.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-concat-10.smt.log: extract-concat-10.smt
+	@p='extract-concat-10.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-concat-11.smt.log: extract-concat-11.smt
+	@p='extract-concat-11.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-constant.smt.log: extract-constant.smt
+	@p='extract-constant.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-extract-0.smt.log: extract-extract-0.smt
+	@p='extract-extract-0.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-extract-1.smt.log: extract-extract-1.smt
+	@p='extract-extract-1.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-extract-2.smt.log: extract-extract-2.smt
+	@p='extract-extract-2.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-extract-3.smt.log: extract-extract-3.smt
+	@p='extract-extract-3.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-extract-4.smt.log: extract-extract-4.smt
+	@p='extract-extract-4.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-extract-5.smt.log: extract-extract-5.smt
+	@p='extract-extract-5.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-extract-6.smt.log: extract-extract-6.smt
+	@p='extract-extract-6.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-extract-7.smt.log: extract-extract-7.smt
+	@p='extract-extract-7.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-extract-8.smt.log: extract-extract-8.smt
+	@p='extract-extract-8.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-extract-9.smt.log: extract-extract-9.smt
+	@p='extract-extract-9.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-extract-10.smt.log: extract-extract-10.smt
+	@p='extract-extract-10.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-extract-11.smt.log: extract-extract-11.smt
+	@p='extract-extract-11.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-whole-0.smt.log: extract-whole-0.smt
+	@p='extract-whole-0.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-whole-1.smt.log: extract-whole-1.smt
+	@p='extract-whole-1.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-whole-2.smt.log: extract-whole-2.smt
+	@p='extract-whole-2.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-whole-3.smt.log: extract-whole-3.smt
+	@p='extract-whole-3.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+extract-whole-4.smt.log: extract-whole-4.smt
+	@p='extract-whole-4.smt'; $(am__check_pre) $(LOG_COMPILE) "$$tst" $(am__check_post)
+.test.log:
+	@p='$<'; $(am__check_pre) $(TEST_LOG_COMPILE) "$$tst" $(am__check_post)
+@am__EXEEXT_TRUE@.test$(EXEEXT).log:
+@am__EXEEXT_TRUE@	@p='$<'; $(am__check_pre) $(TEST_LOG_COMPILE) "$$tst" $(am__check_post)
+
+distdir: $(DISTFILES)
+	@srcdirstrip=`echo "$(srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \
+	topsrcdirstrip=`echo "$(top_srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \
+	list='$(DISTFILES)'; \
+	  dist_files=`for file in $$list; do echo $$file; done | \
+	  sed -e "s|^$$srcdirstrip/||;t" \
+	      -e "s|^$$topsrcdirstrip/|$(top_builddir)/|;t"`; \
+	case $$dist_files in \
+	  */*) $(MKDIR_P) `echo "$$dist_files" | \
+			   sed '/\//!d;s|^|$(distdir)/|;s,/[^/]*$$,,' | \
+			   sort -u` ;; \
+	esac; \
+	for file in $$dist_files; do \
+	  if test -f $$file || test -d $$file; then d=.; else d=$(srcdir); fi; \
+	  if test -d $$d/$$file; then \
+	    dir=`echo "/$$file" | sed -e 's,/[^/]*$$,,'`; \
+	    if test -d "$(distdir)/$$file"; then \
+	      find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \
+	    fi; \
+	    if test -d $(srcdir)/$$file && test $$d != $(srcdir); then \
+	      cp -fpR $(srcdir)/$$file "$(distdir)$$dir" || exit 1; \
+	      find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \
+	    fi; \
+	    cp -fpR $$d/$$file "$(distdir)$$dir" || exit 1; \
+	  else \
+	    test -f "$(distdir)/$$file" \
+	    || cp -p $$d/$$file "$(distdir)/$$file" \
+	    || exit 1; \
+	  fi; \
+	done
+check-am: all-am
+	$(MAKE) $(AM_MAKEFLAGS) check-TESTS
+check: check-am
+all-am: Makefile
+installdirs:
+install: install-am
+install-exec: install-exec-am
+install-data: install-data-am
+uninstall: uninstall-am
+
+install-am: all-am
+	@$(MAKE) $(AM_MAKEFLAGS) install-exec-am install-data-am
+
+installcheck: installcheck-am
+install-strip:
+	$(MAKE) $(AM_MAKEFLAGS) INSTALL_PROGRAM="$(INSTALL_STRIP_PROGRAM)" \
+	  install_sh_PROGRAM="$(INSTALL_STRIP_PROGRAM)" INSTALL_STRIP_FLAG=-s \
+	  `test -z '$(STRIP)' || \
+	    echo "INSTALL_PROGRAM_ENV=STRIPPROG='$(STRIP)'"` install
+mostlyclean-generic:
+	-test -z "$(TEST_LOGS)" || rm -f $(TEST_LOGS)
+	-test -z "$(TEST_LOGS_TMP)" || rm -f $(TEST_LOGS_TMP)
+	-test -z "$(TEST_SUITE_HTML)" || rm -f $(TEST_SUITE_HTML)
+	-test -z "$(TEST_SUITE_LOG)" || rm -f $(TEST_SUITE_LOG)
+
+clean-generic:
+
+distclean-generic:
+	-test -z "$(CONFIG_CLEAN_FILES)" || rm -f $(CONFIG_CLEAN_FILES)
+	-test . = "$(srcdir)" || test -z "$(CONFIG_CLEAN_VPATH_FILES)" || rm -f $(CONFIG_CLEAN_VPATH_FILES)
+
+maintainer-clean-generic:
+	@echo "This command is intended for maintainers to use"
+	@echo "it deletes files that may require special tools to rebuild."
+clean: clean-am
+
+clean-am: clean-generic clean-libtool mostlyclean-am
+
+distclean: distclean-am
+	-rm -f Makefile
+distclean-am: clean-am distclean-generic
+
+dvi: dvi-am
+
+dvi-am:
+
+html: html-am
+
+html-am:
+
+info: info-am
+
+info-am:
+
+install-data-am:
+
+install-dvi: install-dvi-am
+
+install-dvi-am:
+
+install-exec-am:
+
+install-html: install-html-am
+
+install-html-am:
+
+install-info: install-info-am
+
+install-info-am:
+
+install-man:
+
+install-pdf: install-pdf-am
+
+install-pdf-am:
+
+install-ps: install-ps-am
+
+install-ps-am:
+
+installcheck-am:
+
+maintainer-clean: maintainer-clean-am
+	-rm -f Makefile
+maintainer-clean-am: distclean-am maintainer-clean-generic
+
+mostlyclean: mostlyclean-am
+
+mostlyclean-am: mostlyclean-generic mostlyclean-libtool
+
+pdf: pdf-am
+
+pdf-am:
+
+ps: ps-am
+
+ps-am:
+
+uninstall-am:
+
+.MAKE: check-am check-html install-am install-strip recheck \
+	recheck-html
+
+.PHONY: all all-am check check-TESTS check-am check-html clean \
+	clean-generic clean-libtool distclean distclean-generic \
+	distclean-libtool distdir dvi dvi-am html html-am info info-am \
+	install install-am install-data install-data-am install-dvi \
+	install-dvi-am install-exec install-exec-am install-html \
+	install-html-am install-info install-info-am install-man \
+	install-pdf install-pdf-am install-ps install-ps-am \
+	install-strip installcheck installcheck-am installdirs \
+	maintainer-clean maintainer-clean-generic mostlyclean \
+	mostlyclean-generic mostlyclean-libtool pdf pdf-am ps ps-am \
+	recheck recheck-html uninstall uninstall-am
+
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:
+
+# Tell versions [3.59,3.63) of GNU make to not export all variables.
+# Otherwise a system limit (for SysV at least) may be exceeded.
+.NOEXPORT:
diff --git a/test/regress/regress0/bv/core/concat-merge-0.smt b/test/regress/regress0/bv/core/concat-merge-0.smt
index c68d4ec53..2d4310163 100644
--- a/test/regress/regress0/bv/core/concat-merge-0.smt
+++ b/test/regress/regress0/bv/core/concat-merge-0.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :formula
 (not (= (concat (extract[2:1] x) (extract[0:0] x)) (extract[2:0] x)))
diff --git a/test/regress/regress0/bv/core/concat-merge-1.smt b/test/regress/regress0/bv/core/concat-merge-1.smt
index 4b6702598..e0326288d 100644
--- a/test/regress/regress0/bv/core/concat-merge-1.smt
+++ b/test/regress/regress0/bv/core/concat-merge-1.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :formula
 (not (= (concat (extract[4:2] x) (extract[1:0] x)) (extract[4:0] x)))
diff --git a/test/regress/regress0/bv/core/concat-merge-2.smt b/test/regress/regress0/bv/core/concat-merge-2.smt
index 2350d6d8b..4fe5e597c 100644
--- a/test/regress/regress0/bv/core/concat-merge-2.smt
+++ b/test/regress/regress0/bv/core/concat-merge-2.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :formula
 (not (= (concat (extract[8:4] x) (extract[3:0] x)) (extract[8:0] x)))
diff --git a/test/regress/regress0/bv/core/concat-merge-3.smt b/test/regress/regress0/bv/core/concat-merge-3.smt
index 303357541..64b3010af 100644
--- a/test/regress/regress0/bv/core/concat-merge-3.smt
+++ b/test/regress/regress0/bv/core/concat-merge-3.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :formula
 (not (= (concat (extract[16:8] x) (extract[7:0] x)) (extract[16:0] x)))
diff --git a/test/regress/regress0/bv/core/extract-concat-0.smt b/test/regress/regress0/bv/core/extract-concat-0.smt
index c4d6c7e02..edbbe5cf5 100644
--- a/test/regress/regress0/bv/core/extract-concat-0.smt
+++ b/test/regress/regress0/bv/core/extract-concat-0.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :extrafuns ((y BitVec[32]))
   :formula
diff --git a/test/regress/regress0/bv/core/extract-concat-1.smt b/test/regress/regress0/bv/core/extract-concat-1.smt
index 0f5a2c187..193fc5893 100644
--- a/test/regress/regress0/bv/core/extract-concat-1.smt
+++ b/test/regress/regress0/bv/core/extract-concat-1.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :extrafuns ((y BitVec[32]))
   :formula
diff --git a/test/regress/regress0/bv/core/extract-concat-10.smt b/test/regress/regress0/bv/core/extract-concat-10.smt
index ed44a9abb..65265c709 100644
--- a/test/regress/regress0/bv/core/extract-concat-10.smt
+++ b/test/regress/regress0/bv/core/extract-concat-10.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :extrafuns ((y BitVec[32]))
   :formula
diff --git a/test/regress/regress0/bv/core/extract-concat-11.smt b/test/regress/regress0/bv/core/extract-concat-11.smt
index ed1f6275e..c9b04d4e7 100644
--- a/test/regress/regress0/bv/core/extract-concat-11.smt
+++ b/test/regress/regress0/bv/core/extract-concat-11.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :extrafuns ((y BitVec[32]))
   :formula
diff --git a/test/regress/regress0/bv/core/extract-concat-2.smt b/test/regress/regress0/bv/core/extract-concat-2.smt
index fb8c61464..c08573abc 100644
--- a/test/regress/regress0/bv/core/extract-concat-2.smt
+++ b/test/regress/regress0/bv/core/extract-concat-2.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :extrafuns ((y BitVec[32]))
   :formula
diff --git a/test/regress/regress0/bv/core/extract-concat-3.smt b/test/regress/regress0/bv/core/extract-concat-3.smt
index f89115ecf..86c90dbcd 100644
--- a/test/regress/regress0/bv/core/extract-concat-3.smt
+++ b/test/regress/regress0/bv/core/extract-concat-3.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :extrafuns ((y BitVec[32]))
   :formula
diff --git a/test/regress/regress0/bv/core/extract-concat-4.smt b/test/regress/regress0/bv/core/extract-concat-4.smt
index 29ea62916..380f495db 100644
--- a/test/regress/regress0/bv/core/extract-concat-4.smt
+++ b/test/regress/regress0/bv/core/extract-concat-4.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :extrafuns ((y BitVec[32]))
   :formula
diff --git a/test/regress/regress0/bv/core/extract-concat-5.smt b/test/regress/regress0/bv/core/extract-concat-5.smt
index 8f137ef05..822fedc82 100644
--- a/test/regress/regress0/bv/core/extract-concat-5.smt
+++ b/test/regress/regress0/bv/core/extract-concat-5.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :extrafuns ((y BitVec[32]))
   :formula
diff --git a/test/regress/regress0/bv/core/extract-concat-6.smt b/test/regress/regress0/bv/core/extract-concat-6.smt
index 0ef6e2ee6..23dcadedd 100644
--- a/test/regress/regress0/bv/core/extract-concat-6.smt
+++ b/test/regress/regress0/bv/core/extract-concat-6.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :extrafuns ((y BitVec[32]))
   :formula
diff --git a/test/regress/regress0/bv/core/extract-concat-7.smt b/test/regress/regress0/bv/core/extract-concat-7.smt
index f1a9bf161..4d3bc7c9d 100644
--- a/test/regress/regress0/bv/core/extract-concat-7.smt
+++ b/test/regress/regress0/bv/core/extract-concat-7.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :extrafuns ((y BitVec[32]))
   :formula
diff --git a/test/regress/regress0/bv/core/extract-concat-8.smt b/test/regress/regress0/bv/core/extract-concat-8.smt
index c317e94e1..f6dc143ef 100644
--- a/test/regress/regress0/bv/core/extract-concat-8.smt
+++ b/test/regress/regress0/bv/core/extract-concat-8.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :extrafuns ((y BitVec[32]))
   :formula
diff --git a/test/regress/regress0/bv/core/extract-concat-9.smt b/test/regress/regress0/bv/core/extract-concat-9.smt
index 668842dfc..17870bdbb 100644
--- a/test/regress/regress0/bv/core/extract-concat-9.smt
+++ b/test/regress/regress0/bv/core/extract-concat-9.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :extrafuns ((y BitVec[32]))
   :formula
diff --git a/test/regress/regress0/bv/core/extract-constant.smt b/test/regress/regress0/bv/core/extract-constant.smt
index a36bb6ea7..bfa338957 100644
--- a/test/regress/regress0/bv/core/extract-constant.smt
+++ b/test/regress/regress0/bv/core/extract-constant.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :formula
 (not (= (extract[6:2] bv56[9]) bv14[5]))
 )
diff --git a/test/regress/regress0/bv/core/extract-extract-0.smt b/test/regress/regress0/bv/core/extract-extract-0.smt
index 971ad9e8d..5ec2bcf1c 100644
--- a/test/regress/regress0/bv/core/extract-extract-0.smt
+++ b/test/regress/regress0/bv/core/extract-extract-0.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :formula
 (let (?cvc_0 (extract[31:0] x)) (not (= (extract[31:0] ?cvc_0) ?cvc_0)))
diff --git a/test/regress/regress0/bv/core/extract-extract-1.smt b/test/regress/regress0/bv/core/extract-extract-1.smt
index 098e417b9..e57d85e9d 100644
--- a/test/regress/regress0/bv/core/extract-extract-1.smt
+++ b/test/regress/regress0/bv/core/extract-extract-1.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :formula
 (not (= (extract[15:1] (extract[31:0] x)) (extract[15:1] x)))
diff --git a/test/regress/regress0/bv/core/extract-extract-10.smt b/test/regress/regress0/bv/core/extract-extract-10.smt
index d277f5fdb..d806c6e39 100644
--- a/test/regress/regress0/bv/core/extract-extract-10.smt
+++ b/test/regress/regress0/bv/core/extract-extract-10.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :formula
 (not (= (extract[2:2] (extract[7:2] x)) (extract[4:4] x)))
diff --git a/test/regress/regress0/bv/core/extract-extract-11.smt b/test/regress/regress0/bv/core/extract-extract-11.smt
index 189c7ef47..488b22f1b 100644
--- a/test/regress/regress0/bv/core/extract-extract-11.smt
+++ b/test/regress/regress0/bv/core/extract-extract-11.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :formula
 (not (= (extract[0:0] (extract[8:7] (extract[14:6] (extract[19:5] (extract[23:4] (extract[26:3] (extract[28:2] (extract[30:1] x)))))))) (extract[28:28] x)))
diff --git a/test/regress/regress0/bv/core/extract-extract-2.smt b/test/regress/regress0/bv/core/extract-extract-2.smt
index f423ec9ad..86f61bf33 100644
--- a/test/regress/regress0/bv/core/extract-extract-2.smt
+++ b/test/regress/regress0/bv/core/extract-extract-2.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :formula
 (not (= (extract[7:2] (extract[31:0] x)) (extract[7:2] x)))
diff --git a/test/regress/regress0/bv/core/extract-extract-3.smt b/test/regress/regress0/bv/core/extract-extract-3.smt
index e614c4c92..27237023b 100644
--- a/test/regress/regress0/bv/core/extract-extract-3.smt
+++ b/test/regress/regress0/bv/core/extract-extract-3.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :formula
 (not (= (extract[4:4] (extract[31:0] x)) (extract[4:4] x)))
diff --git a/test/regress/regress0/bv/core/extract-extract-4.smt b/test/regress/regress0/bv/core/extract-extract-4.smt
index 2b9c92946..f8df127b0 100644
--- a/test/regress/regress0/bv/core/extract-extract-4.smt
+++ b/test/regress/regress0/bv/core/extract-extract-4.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :formula
 (let (?cvc_0 (extract[15:1] x)) (not (= (extract[14:0] ?cvc_0) ?cvc_0)))
diff --git a/test/regress/regress0/bv/core/extract-extract-5.smt b/test/regress/regress0/bv/core/extract-extract-5.smt
index 0623ce997..4179cc330 100644
--- a/test/regress/regress0/bv/core/extract-extract-5.smt
+++ b/test/regress/regress0/bv/core/extract-extract-5.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :formula
 (not (= (extract[7:1] (extract[15:1] x)) (extract[8:2] x)))
diff --git a/test/regress/regress0/bv/core/extract-extract-6.smt b/test/regress/regress0/bv/core/extract-extract-6.smt
index 851bd6f68..33220b21f 100644
--- a/test/regress/regress0/bv/core/extract-extract-6.smt
+++ b/test/regress/regress0/bv/core/extract-extract-6.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :formula
 (not (= (extract[3:2] (extract[15:1] x)) (extract[4:3] x)))
diff --git a/test/regress/regress0/bv/core/extract-extract-7.smt b/test/regress/regress0/bv/core/extract-extract-7.smt
index e6a2acc13..5407c221c 100644
--- a/test/regress/regress0/bv/core/extract-extract-7.smt
+++ b/test/regress/regress0/bv/core/extract-extract-7.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :formula
 (not (= (extract[3:3] (extract[15:1] x)) (extract[4:4] x)))
diff --git a/test/regress/regress0/bv/core/extract-extract-8.smt b/test/regress/regress0/bv/core/extract-extract-8.smt
index 7a808f31a..785ba442e 100644
--- a/test/regress/regress0/bv/core/extract-extract-8.smt
+++ b/test/regress/regress0/bv/core/extract-extract-8.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :formula
 (let (?cvc_0 (extract[7:2] x)) (not (= (extract[5:0] ?cvc_0) ?cvc_0)))
diff --git a/test/regress/regress0/bv/core/extract-extract-9.smt b/test/regress/regress0/bv/core/extract-extract-9.smt
index 7a3c8e3da..27e997895 100644
--- a/test/regress/regress0/bv/core/extract-extract-9.smt
+++ b/test/regress/regress0/bv/core/extract-extract-9.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :formula
 (not (= (extract[3:1] (extract[7:2] x)) (extract[5:3] x)))
diff --git a/test/regress/regress0/bv/core/extract-whole-0.smt b/test/regress/regress0/bv/core/extract-whole-0.smt
index 83025250f..5464f9114 100644
--- a/test/regress/regress0/bv/core/extract-whole-0.smt
+++ b/test/regress/regress0/bv/core/extract-whole-0.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :formula
 (not (= (concat (concat (concat (concat (concat (concat bv0[1] (extract[31:31] x)) (extract[30:20] x)) (extract[19:10] x)) (extract[9:1] x)) (extract[0:0] x)) bv0[1]) (concat (concat bv0[1] x) bv0[1])))
diff --git a/test/regress/regress0/bv/core/extract-whole-1.smt b/test/regress/regress0/bv/core/extract-whole-1.smt
index bc74e0ca9..67f55b0c3 100644
--- a/test/regress/regress0/bv/core/extract-whole-1.smt
+++ b/test/regress/regress0/bv/core/extract-whole-1.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :formula
 (not (= (concat (concat (concat (concat (extract[31:31] x) (extract[30:20] x)) (extract[19:10] x)) (extract[9:1] x)) (extract[0:0] x)) x))
diff --git a/test/regress/regress0/bv/core/extract-whole-2.smt b/test/regress/regress0/bv/core/extract-whole-2.smt
index c661678eb..5e016f6de 100644
--- a/test/regress/regress0/bv/core/extract-whole-2.smt
+++ b/test/regress/regress0/bv/core/extract-whole-2.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :formula
 (not (= (concat (concat (concat (concat (concat (concat x bv0[1]) bv1[1]) bv0[1]) bv1[1]) bv0[1]) bv1[1]) (concat x bv21[6])))
diff --git a/test/regress/regress0/bv/core/extract-whole-3.smt b/test/regress/regress0/bv/core/extract-whole-3.smt
index 2767384af..42464cbf4 100644
--- a/test/regress/regress0/bv/core/extract-whole-3.smt
+++ b/test/regress/regress0/bv/core/extract-whole-3.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :formula
 (not (= (concat (concat (concat (concat (concat (concat bv0[1] bv1[1]) bv0[1]) bv1[1]) bv0[1]) bv1[1]) x) (concat bv21[6] x)))
diff --git a/test/regress/regress0/bv/core/extract-whole-4.smt b/test/regress/regress0/bv/core/extract-whole-4.smt
index 41d2f0594..c26b2173b 100644
--- a/test/regress/regress0/bv/core/extract-whole-4.smt
+++ b/test/regress/regress0/bv/core/extract-whole-4.smt
@@ -1,5 +1,6 @@
 (benchmark B_
   :logic QF_BV
+  :status unsat
   :extrafuns ((x BitVec[32]))
   :formula
 (not (= (extract[31:0] x) x))