blu='\e[1;34m'; \
std='\e[m'; \
}
-subdirs_to_check = unit system regress/regress0 regress/regress0/arith regress/regress0/uf regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3
+subdirs_to_check = unit system regress/regress0 regress/regress0/arith regress/regress0/uf regress/regress0/bv regress/regress0/bv/core regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3
check-recursive: check-pre
.PHONY: check-pre
check-pre:
-SUBDIRS = . arith precedence uf
+SUBDIRS = . arith precedence uf bv
TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
MAKEFLAGS = -k
--- /dev/null
+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)
+
--- /dev/null
+# 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='\e[0;31m'; \
+ grn='\e[0;32m'; \
+ lgn='\e[1;32m'; \
+ blu='\e[1;34m'; \
+ std='\e[m'; \
+}
+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:
--- /dev/null
+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:
--- /dev/null
+# 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='\e[0;31m'; \
+ grn='\e[0;32m'; \
+ lgn='\e[1;32m'; \
+ blu='\e[1;34m'; \
+ std='\e[m'; \
+}
+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:
(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)))
(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)))
(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)))
(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)))
(benchmark B_
:logic QF_BV
+ :status unsat
:extrafuns ((x BitVec[32]))
:extrafuns ((y BitVec[32]))
:formula
(benchmark B_
:logic QF_BV
+ :status unsat
:extrafuns ((x BitVec[32]))
:extrafuns ((y BitVec[32]))
:formula
(benchmark B_
:logic QF_BV
+ :status unsat
:extrafuns ((x BitVec[32]))
:extrafuns ((y BitVec[32]))
:formula
(benchmark B_
:logic QF_BV
+ :status unsat
:extrafuns ((x BitVec[32]))
:extrafuns ((y BitVec[32]))
:formula
(benchmark B_
:logic QF_BV
+ :status unsat
:extrafuns ((x BitVec[32]))
:extrafuns ((y BitVec[32]))
:formula
(benchmark B_
:logic QF_BV
+ :status unsat
:extrafuns ((x BitVec[32]))
:extrafuns ((y BitVec[32]))
:formula
(benchmark B_
:logic QF_BV
+ :status unsat
:extrafuns ((x BitVec[32]))
:extrafuns ((y BitVec[32]))
:formula
(benchmark B_
:logic QF_BV
+ :status unsat
:extrafuns ((x BitVec[32]))
:extrafuns ((y BitVec[32]))
:formula
(benchmark B_
:logic QF_BV
+ :status unsat
:extrafuns ((x BitVec[32]))
:extrafuns ((y BitVec[32]))
:formula
(benchmark B_
:logic QF_BV
+ :status unsat
:extrafuns ((x BitVec[32]))
:extrafuns ((y BitVec[32]))
:formula
(benchmark B_
:logic QF_BV
+ :status unsat
:extrafuns ((x BitVec[32]))
:extrafuns ((y BitVec[32]))
:formula
(benchmark B_
:logic QF_BV
+ :status unsat
:extrafuns ((x BitVec[32]))
:extrafuns ((y BitVec[32]))
:formula
(benchmark B_
:logic QF_BV
+ :status unsat
:formula
(not (= (extract[6:2] bv56[9]) bv14[5]))
)
(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)))
(benchmark B_
:logic QF_BV
+ :status unsat
:extrafuns ((x BitVec[32]))
:formula
(not (= (extract[15:1] (extract[31:0] x)) (extract[15:1] x)))
(benchmark B_
:logic QF_BV
+ :status unsat
:extrafuns ((x BitVec[32]))
:formula
(not (= (extract[2:2] (extract[7:2] x)) (extract[4:4] x)))
(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)))
(benchmark B_
:logic QF_BV
+ :status unsat
:extrafuns ((x BitVec[32]))
:formula
(not (= (extract[7:2] (extract[31:0] x)) (extract[7:2] x)))
(benchmark B_
:logic QF_BV
+ :status unsat
:extrafuns ((x BitVec[32]))
:formula
(not (= (extract[4:4] (extract[31:0] x)) (extract[4:4] x)))
(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)))
(benchmark B_
:logic QF_BV
+ :status unsat
:extrafuns ((x BitVec[32]))
:formula
(not (= (extract[7:1] (extract[15:1] x)) (extract[8:2] x)))
(benchmark B_
:logic QF_BV
+ :status unsat
:extrafuns ((x BitVec[32]))
:formula
(not (= (extract[3:2] (extract[15:1] x)) (extract[4:3] x)))
(benchmark B_
:logic QF_BV
+ :status unsat
:extrafuns ((x BitVec[32]))
:formula
(not (= (extract[3:3] (extract[15:1] x)) (extract[4:4] x)))
(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)))
(benchmark B_
:logic QF_BV
+ :status unsat
:extrafuns ((x BitVec[32]))
:formula
(not (= (extract[3:1] (extract[7:2] x)) (extract[5:3] x)))
(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])))
(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))
(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])))
(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)))
(benchmark B_
:logic QF_BV
+ :status unsat
:extrafuns ((x BitVec[32]))
:formula
(not (= (extract[31:0] x) x))
projects / cvc5.git / commitdiff