From: Dejan Jovanović Date: Mon, 20 Sep 2010 16:47:38 +0000 (+0000) Subject: hooking up the bitvector tests X-Git-Tag: cvc5-1.0.0~8863 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d3d08250a1ec33689ec29736600c17aab7614d18;p=cvc5.git hooking up the bitvector tests --- diff --git a/test/Makefile.am b/test/Makefile.am index a257b96d9..2ff1c4974 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -26,7 +26,7 @@ test "X$(AM_COLOR_TESTS)" != Xno \ blu=''; \ std=''; \ } -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: 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))