From nobody Tue Nov 01 01:12:06 2022 X-Original-To: pkg-fallout@mlmmj.nyi.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2610:1c1:1:606c::19:1]) by mlmmj.nyi.freebsd.org (Postfix) with ESMTP id 4N1X6t5kd4z4h1tf for ; Tue, 1 Nov 2022 01:12:06 +0000 (UTC) (envelope-from pkg-fallout@FreeBSD.org) Received: from mxrelay.nyi.freebsd.org (mxrelay.nyi.freebsd.org [IPv6:2610:1c1:1:606c::19:3]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256 client-signature RSA-PSS (4096 bits) client-digest SHA256) (Client CN "mxrelay.nyi.freebsd.org", Issuer "R3" (verified OK)) by mx1.freebsd.org (Postfix) with ESMTPS id 4N1X6t2yrhz3XCL for ; Tue, 1 Nov 2022 01:12:06 +0000 (UTC) (envelope-from pkg-fallout@FreeBSD.org) Received: from beefy13.nyi.freebsd.org (beefy13.nyi.freebsd.org [IPv6:2610:1c1:1:6080::16:1c]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (Client did not present a certificate) by mxrelay.nyi.freebsd.org (Postfix) with ESMTPS id 4N1X6t20yGzxKT for ; Tue, 1 Nov 2022 01:12:06 +0000 (UTC) (envelope-from pkg-fallout@FreeBSD.org) Received: from beefy13.nyi.freebsd.org (localhost [127.0.0.1]) by beefy13.nyi.freebsd.org (8.16.1/8.16.1) with ESMTP id 2A11C6tC056737 for ; Tue, 1 Nov 2022 01:12:06 GMT (envelope-from pkg-fallout@FreeBSD.org) Received: (from root@localhost) by beefy13.nyi.freebsd.org (8.16.1/8.16.1/Submit) id 2A11C63e056732; Tue, 1 Nov 2022 01:12:06 GMT (envelope-from pkg-fallout@FreeBSD.org) Date: Tue, 1 Nov 2022 01:12:06 GMT From: pkg-fallout@FreeBSD.org Message-Id: <202211010112.2A11C63e056732@beefy13.nyi.freebsd.org> To: pkg-fallout@FreeBSD.org Subject: [package - 131i386-quarterly][math/cvc4] Failed for cvc4-1.7_6 in build ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1667265126; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc; bh=ySVDU+GPhBjUHdGJmUoN0pr3pRIdvx7Yuh6ZSWOBbJ4=; b=yONfTz9rCde0AVYkHcMAxthq6+yRoMlxsxUrn+fbDm+m6xIss05QfhX5zMSxM0IsB0qmdu uNy0dpGNmLzSWytYJmFKG+gf4/jvTHc4pvy8u0Ukmt4G9l1q3+Yg1IpgDpKA50Z9N+oGS9 CQf5spqR2XDMlncXqXewaABmAKMejsMrOB/x9JqYcCF5FwixGMxUL3t7QSG/jv8o7s7ooa Iu2sCSY1px1N0Mi6gPHpLzMJoclVEqaQ5sNYu4B2+1ejx0Flsb5eUB/9SGJ8MB3lwagwPE 8gbmUyXpIcUM/gy04LekGZiuBipb6jeAZ4S7i5LkrmTtSeUFRti/AGis39D4LQ== ARC-Seal: i=1; s=dkim; d=freebsd.org; t=1667265126; a=rsa-sha256; cv=none; b=IE49kpglQRCqkc+e2uUvho0JQfsHUAE00s/CllrFLSn3tnWxowqfAVHRt6IOt2JyQrGqYA MhKUAidJwsKKNgvavT2qNoV9AdBgJPnCuXlaYuTYbc4TAAI8ySzpIwIZRrMqdF+daxAnQD 2mUq1bfBrreG7iVpVc+HRWirsFwIvkW/fxB1nfcMHE0lZ5/cVqJRIqWODv8FiRTbu71zJq bczWwGYtIFfBX8Dnfj1cMtAllO06qSLyBCs+mudTw+PIf1hKnfGsQa/U7EkpEMmRILjuI+ JGR3RLmHTQKdukHnb94Wc31hVYSFTYz1PzMOf686HGpJd7uP9VV4CV/ds7ZmFg== ARC-Authentication-Results: i=1; mx1.freebsd.org; none X-ThisMailContainsUnwantedMimeParts: N List-Id: Fallout logs from package building List-Archive: https://lists.freebsd.org/archives/freebsd-pkg-fallout List-Help: List-Post: List-Subscribe: List-Unsubscribe: Sender: owner-freebsd-pkg-fallout@freebsd.org You are receiving this mail as a port that you maintain is failing to build on the FreeBSD package build server. Please investigate the failure and submit a PR to fix build. Maintainer: ports@FreeBSD.org Log URL: http://beefy13.nyi.freebsd.org/data/131i386-quarterly/8ef5d08e2f64/logs/cvc4-1.7_6.log Build URL: http://beefy13.nyi.freebsd.org/build.html?mastername=131i386-quarterly&build=8ef5d08e2f64 Log: =>> Building math/cvc4 build started at Tue Nov 1 01:11:15 UTC 2022 port directory: /usr/ports/math/cvc4 package name: cvc4-1.7_6 building for: FreeBSD 131i386-quarterly-job-12 13.1-RELEASE-p2 FreeBSD 13.1-RELEASE-p2 i386 maintained by: ports@FreeBSD.org Makefile ident: Poudriere version: 3.2.8-21-g883afb07 Host OSVERSION: 1400063 Jail OSVERSION: 1301000 Job Id: 12 ---Begin Environment--- SHELL=/bin/csh UNAME_p=i386 UNAME_m=i386 OSVERSION=1301000 UNAME_v=FreeBSD 13.1-RELEASE-p2 UNAME_r=13.1-RELEASE-p2 BLOCKSIZE=K MAIL=/var/mail/root MM_CHARSET=UTF-8 LANG=C.UTF-8 STATUS=1 HOME=/root PATH=/sbin:/bin:/usr/sbin:/usr/bin:/usr/local/sbin:/usr/local/bin:/root/bin LOCALBASE=/usr/local USER=root LIBEXECPREFIX=/usr/local/libexec/poudriere POUDRIERE_VERSION=3.2.8-21-g883afb07 MASTERMNT=/usr/local/poudriere/data/.m/131i386-quarterly/ref POUDRIERE_BUILD_TYPE=bulk PACKAGE_BUILDING=yes SAVED_TERM= PWD=/usr/local/poudriere/data/.m/131i386-quarterly/ref/.p/pool P_PORTS_FEATURES=FLAVORS SELECTED_OPTIONS MASTERNAME=131i386-quarterly SCRIPTPREFIX=/usr/local/share/poudriere OLDPWD=/usr/local/poudriere/data/.m/131i386-quarterly/ref/.p SCRIPTPATH=/usr/local/share/poudriere/bulk.sh POUDRIEREPATH=/usr/local/bin/poudriere ---End Environment--- ---Begin Poudriere Port Flags/Env--- PORT_FLAGS= PKGENV= FLAVOR= DEPENDS_ARGS= MAKE_ARGS= ---End Poudriere Port Flags/Env--- ---Begin OPTIONS List--- ===> The following configuration options are available for cvc4-1.7_6: CRYPTOMINISAT=on: Use CryptoMiniSat as the SAT solver JAVA=on: Java platform support PYTHON=on: Python bindings or support READLINE=on: Command line editing via libreadline ====> Options available for the radio NUMLIB: you can only select none or one of them GMP=on: Use GMP numeric library CLN=off: Use CLN numeric library (disables portfolio mode) ===> Use 'make config' to modify these settings ---End OPTIONS List--- --MAINTAINER-- ports@FreeBSD.org --End MAINTAINER-- --CONFIGURE_ARGS-- --End CONFIGURE_ARGS-- --CONFIGURE_ENV-- PKG_CONFIG=pkgconf PYTHON="/usr/local/bin/python3.9" XDG_DATA_HOME=/wrkdirs/usr/ports/math/cvc4/work XDG_CONFIG_HOME=/wrkdirs/usr/ports/math/cvc4/work XDG_CACHE_HOME=/wrkdirs/usr/ports/math/cvc4/work/.cache HOME=/wrkdirs/usr/ports/math/cvc4/work TMPDIR="/tmp" PATH=/wrkdirs/usr/ports/math/cvc4/work/.bin:/sbin:/bin:/usr/sbin:/usr/bin:/usr/local/sbin:/usr/local/bin:/root/bin PKG_CONFIG_LIBDIR=/wrkdirs/usr/ports/math/cvc4/work/.pkgconfig:/usr/local/libdata/pkgconfig:/usr/local/share/pkgconfig:/usr/libdata/pkgconfig SHELL=/bin/sh CONFIG_SHELL=/bin/sh --End CONFIGURE_ENV-- --MAKE_ENV-- NINJA_STATUS="[%p %s/%t] " XDG_DATA_HOME=/wrkdirs/usr/ports/math/cvc4/work XDG_CONFIG_HOME=/wrkdirs/usr/ports/math/cvc4/work XDG_CACHE_HOME=/wrkdirs/usr/ports/math/cvc4/work/.cache HOME=/wrkdirs/usr/ports/math/cvc4/work TMPDIR="/tmp" PATH=/wrkdirs/usr/ports/math/cvc4/work/.bin:/sbin:/bin:/usr/sbin:/usr/bin:/usr/local/sbin:/usr/local/bin:/root/bin PKG_CONFIG_LIBDIR=/wrkdirs/usr/ports/math/cvc4/work/.pkgconfig:/usr/local/libdata/pkgconfig:/usr/local/share/pkgconfig:/usr/libdata/pkgconfig NO_PIE=yes MK_DEBUG_FILES=no MK_KERNEL_SYMBOLS=no SHELL=/bin/sh NO_LINT=YES DESTDIR=/wrkdirs/usr/ports/math/cvc4/work/stage PREFIX=/usr/local LOCALBASE=/usr/local CC="cc" CFLAGS="-O2 -pipe -fstack-protector-strong -fno-strict-aliasing " CPP="cpp" CPPFLAGS="-I/usr/local/include" LDFLAGS=" -L/usr/local/lib -fstack-protector-strong " LIBS="" CXX="c++" CXXFLAGS="-O2 -pipe -fstack-protector-strong -fno-strict-aliasing " MANPREFIX="/usr/local" BSD_INSTALL_PROGRAM="install -s -m 555" BSD_INSTALL_ LIB="install -s -m 0644" BSD_INSTALL_SCRIPT="install -m 555" BSD_INSTALL_DATA="install -m 0644" BSD_INSTALL_MAN="install -m 444" --End MAKE_ENV-- --PLIST_SUB-- CLN="@comment " NO_CLN="" CRYPTOMINISAT="" NO_CRYPTOMINISAT="@comment " GMP="" NO_GMP="@comment " JAVA="" NO_JAVA="@comment " PYTHON="" NO_PYTHON="@comment " READLINE="" NO_READLINE="@comment " JAVASHAREDIR="share/java" JAVAJARDIR="share/java/classes" CMAKE_BUILD_TYPE="production" PYTHON_INCLUDEDIR=include/python3.9 PYTHON_LIBDIR=lib/python3.9 PYTHON_PLATFORM=freebsd13 PYTHON_SITELIBDIR=lib/python3.9/site-packages PYTHON_SUFFIX=39 PYTHON_EXT_SUFFIX=.cpython-39 PYTHON_VER=3.9 PYTHON_VERSION=python3.9 PYTHON2="@comment " PYTHON3="" OSREL=13.1 PREFIX=%D LOCALBASE=/usr/local RESETPREFIX=/usr/local LIB32DIR=lib DOCSDIR="share/doc/cvc4" EXAMPLESDIR="share/examples/cvc4" DATADIR="share/cvc4" WWWDIR="www/cvc4" ETCDIR="etc/cvc4" --End PLIST_SUB-- --SUB_LIST-- CLN="@comment " NO_CLN="" CRYPTOMINISAT="" NO_CRYPTOMINISAT="@comment " GMP="" NO_GMP="@comment " JAVA="" NO_JAVA="@comment " PYTHON="" NO_PYTHON="@comment " READLINE="" NO_READLINE="@comment " JAVASHAREDIR="/usr/local/share/java" JAVAJARDIR="/usr/local/share/java/classes" JAVALIBDIR="/usr/local/share/java/classes" PREFIX=/usr/local LOCALBASE=/usr/local DATADIR=/usr/local/share/cvc4 DOCSDIR=/usr/local/share/doc/cvc4 EXAMPLESDIR=/usr/local/share/examples/cvc4 WWWDIR=/usr/local/www/cvc4 ETCDIR=/usr/local/etc/cvc4 --End SUB_LIST-- ---Begin make.conf--- USE_PACKAGE_DEPENDS=yes BATCH=yes WRKDIRPREFIX=/wrkdirs PORTSDIR=/usr/ports PACKAGES=/packages DISTDIR=/distfiles PACKAGE_BUILDING=yes PACKAGE_BUILDING_FLAVORS=yes MACHINE=i386 MACHINE_ARCH=i386 ARCH=${MACHINE_ARCH} #### /usr/local/etc/poudriere.d/make.conf #### # XXX: We really need this but cannot use it while 'make checksum' does not # try the next mirror on checksum failure. It currently retries the same # failed mirror and then fails rather then trying another. It *does* # try the next if the size is mismatched though. #MASTER_SITE_FREEBSD=yes # Build ALLOW_MAKE_JOBS_PACKAGES with 2 jobs MAKE_JOBS_NUMBER=2 #### /usr/ports/Mk/Scripts/ports_env.sh #### _CCVERSION_921dbbb2=FreeBSD clang version 13.0.0 (git@github.com:llvm/llvm-project.git llvmorg-13.0.0-0-gd7b669b3a303) Target: i386-unknown-freebsd13.1 Thread model: posix InstalledDir: /usr/bin _ALTCCVERSION_921dbbb2=none _CXXINTERNAL_acaad9ca=FreeBSD clang version 13.0.0 (git@github.com:llvm/llvm-project.git llvmorg-13.0.0-0-gd7b669b3a303) Target: i386-unknown-freebsd13.1 Thread model: posix InstalledDir: /usr/bin "/usr/bin/ld" "--eh-frame-hdr" "-dynamic-linker" "/libexec/ld-elf.so.1" "--hash-style=both" "--enable-new-dtags" "-m" "elf_i386_fbsd" "-o" "a.out" "/usr/lib/crt1.o" "/usr/lib/crti.o" "/usr/lib/crtbegin.o" "-L/usr/lib" "/dev/null" "-lc++" "-lm" "-lgcc" "--as-needed" "-lgcc_s" "--no-as-needed" "-lc" "-lgcc" "--as-needed" "-lgcc_s" "--no-as-needed" "/usr/lib/crtend.o" "/usr/lib/crtn.o" CC_OUTPUT_921dbbb2_58173849=yes CC_OUTPUT_921dbbb2_9bdba57c=yes CC_OUTPUT_921dbbb2_6a4fe7f5=yes CC_OUTPUT_921dbbb2_6bcac02b=yes CC_OUTPUT_921dbbb2_67d20829=yes CC_OUTPUT_921dbbb2_bfa62e83=yes CC_OUTPUT_921dbbb2_f0b4d593=yes CC_OUTPUT_921dbbb2_308abb44=yes CC_OUTPUT_921dbbb2_f00456e5=yes CC_OUTPUT_921dbbb2_65ad290d=yes CC_OUTPUT_921dbbb2_f2776b26=yes CC_OUTPUT_921dbbb2_53255a77=yes CC_OUTPUT_921dbbb2_911cfe02=yes CC_OUTPUT_921dbbb2_b2657cc3=yes CC_OUTPUT_921dbbb2_380987f7=yes CC_OUTPUT_921dbbb2_160933ec=yes CC_OUTPUT_921dbbb2_fb62803b=yes CC_OUTPUT_921dbbb2_af59ad06=yes CC_OUTPUT_921dbbb2_a15f3fcf=yes _OBJC_CCVERSION_921dbbb2=FreeBSD clang version 13.0.0 (git@github.com:llvm/llvm-project.git llvmorg-13.0.0-0-gd7b669b3a303) Target: i386-unknown-freebsd13.1 Thread model: posix InstalledDir: /usr/bin _OBJC_ALTCCVERSION_921dbbb2=none ARCH=i386 OPSYS=FreeBSD _OSRELEASE=13.1-RELEASE-p2 OSREL=13.1 OSVERSION=1301000 PYTHONBASE=/usr/local CONFIGURE_MAX_CMD_LEN=524288 HAVE_PORTS_ENV=1 #### Misc Poudriere #### GID=0 UID=0 ---End make.conf--- --Resource limits-- cpu time (seconds, -t) unlimited file size (512-blocks, -f) unlimited data seg size (kbytes, -d) 524288 stack size (kbytes, -s) 65536 core file size (512-blocks, -c) unlimited max memory size (kbytes, -m) unlimited locked memory (kbytes, -l) unlimited max user processes (-u) 89999 open files (-n) 1024 virtual mem size (kbytes, -v) unlimited swap limit (kbytes, -w) unlimited socket buffer size (bytes, -b) unlimited pseudo-terminals (-p) unlimited kqueues (-k) unlimited umtx shared locks (-o) unlimited --End resource limits-- =================================================== ===> NOTICE: The cvc4 port currently does not have a maintainer. As a result, it is more likely to have unresolved issues, not be up-to-date, or even be removed in the future. To volunteer to maintain this port, please create an issue at: https://bugs.freebsd.org/bugzilla More information about port maintainership is available at: https://docs.freebsd.org/en/articles/contributing/#ports-contributing ===> License GPLv3 accepted by the user =========================================================================== =================================================== ===> cvc4-1.7_6 depends on file: /usr/local/sbin/pkg - not found ===> Installing existing package /packages/All/pkg-1.18.4.pkg [131i386-quarterly-job-12] Installing pkg-1.18.4... [131i386-quarterly-job-12] Extracting pkg-1.18.4: .......... done ===> cvc4-1.7_6 depends on file: /usr/local/sbin/pkg - found ===> Returning to build of cvc4-1.7_6 =========================================================================== =================================================== =========================================================================== =================================================== ===> NOTICE: The cvc4 port currently does not have a maintainer. As a result, it is more likely to have unresolved issues, not be up-to-date, or even be removed in the future. To volunteer to maintain this port, please create an issue at: https://bugs.freebsd.org/bugzilla More information about port maintainership is available at: https://docs.freebsd.org/en/articles/contributing/#ports-contributing -- Performing Test CVC4_NEED_INT64_T_OVERLOADS - Success -- Performing Test CVC4_NEED_HASH_UINT64_T_OVERLOAD -- Performing Test CVC4_NEED_HASH_UINT64_T_OVERLOAD - Failed -- Looking for unistd.h -- Looking for unistd.h - found -- Looking for C++ include ext/stdio_filebuf.h -- Looking for C++ include ext/stdio_filebuf.h - not found -- Looking for clock_gettime -- Looking for clock_gettime - found -- Looking for ffs -- Looking for ffs - found -- Looking for optreset -- Looking for optreset - found -- Looking for sigaltstack -- Looking for sigaltstack - found -- Looking for strerror_r -- Looking for strerror_r - found -- Looking for strtok_r -- Looking for strtok_r - found -- Performing Test STRERROR_R_CHAR_P -- Performing Test STRERROR_R_CHAR_P - Failed -- Found Boost: /usr/local/include (found suitable version "1.80.0", minimum required is "1.50.0") -- Found Java: /usr/local/bin/java (found version "1.8.0.342") -- Could NOT find Git (missing: GIT_EXECUTABLE) -- Looking for antlr3FileStreamNew -- Looking for antlr3FileStreamNew - found -- Found ANTLR: /wrkdirs/usr/ports/math/cvc4/work/antlr3 -- Found ANTLR libs: /usr/local/lib/libantlr3c.so -- Found Java: /usr/local/bin/java (found version "1.8.0.342") found components: Runtime -- Found SWIG: /usr/local/bin/swig (found suitable version "4.0.2", minimum required is "3.0.0") -- Found Java: /usr/local/bin/java (found version "1.8.0.342") -- Found JNI: /usr/local/openjdk8/include found components: AWT JVM CMake Warning (dev) at /usr/local/share/cmake/Modules/UseSWIG.cmake:775 (message): Policy CMP0078 is not set: UseSWIG generates standard target names. Run "cmake --help-policy CMP0078" for policy details. Use the cmake_policy command to set the policy and suppress this warning. Call Stack (most recent call first): src/bindings/java/CMakeLists.txt:14 (swig_add_library) This warning is for project developers. Use -Wno-dev to suppress it. CMake Warning (dev) at /usr/local/share/cmake/Modules/UseSWIG.cmake:617 (message): Policy CMP0086 is not set: UseSWIG honors SWIG_MODULE_NAME via -module flag. Run "cmake --help-policy CMP0086" for policy details. Use the cmake_policy command to set the policy and suppress this warning. Call Stack (most recent call first): /usr/local/share/cmake/Modules/UseSWIG.cmake:888 (SWIG_ADD_SOURCE_TO_MODULE) src/bindings/java/CMakeLists.txt:14 (swig_add_library) This warning is for project developers. Use -Wno-dev to suppress it. -- Found PythonLibs: /usr/local/lib/libpython3.9.so (found suitable version "3.9.15", minimum required is "3.9") CMake Warning (dev) at /usr/local/share/cmake/Modules/UseSWIG.cmake:775 (message): Policy CMP0078 is not set: UseSWIG generates standard target names. Run "cmake --help-policy CMP0078" for policy details. Use the cmake_policy command to set the policy and suppress this warning. Call Stack (most recent call first): src/bindings/python/CMakeLists.txt:23 (swig_add_library) This warning is for project developers. Use -Wno-dev to suppress it. CMake Warning (dev) at /usr/local/share/cmake/Modules/UseSWIG.cmake:617 (message): Policy CMP0086 is not set: UseSWIG honors SWIG_MODULE_NAME via -module flag. Run "cmake --help-policy CMP0086" for policy details. Use the cmake_policy command to set the policy and suppress this warning. Call Stack (most recent call first): /usr/local/share/cmake/Modules/UseSWIG.cmake:888 (SWIG_ADD_SOURCE_TO_MODULE) src/bindings/python/CMakeLists.txt:23 (swig_add_library) This warning is for project developers. Use -Wno-dev to suppress it. CVC4 1.7 Build profile : production GPL : on Best configuration : off Optimized : on Optimization level : off Assertions : off Debug symbols : off Debug context mem mgr: off Dumping : off Muzzle : off Proofs : on Replay : off Statistics : on Tracing : off Asan : off Coverage (gcov) : off Profiling (gprof) : off Unit tests : off Valgrind : off Shared libs : on Static binary : off Java bindings : off Python bindings : off Python2 : off Python3 : off Portfolio : off ABC : off CaDiCaL : off CryptoMiniSat : off drat2er : off GLPK : off LFSC : off MP library : gmp Readline : off SymFPU : off CPPLAGS (-D...) : NDEBUG CVC4_PORTFOLIO CVC4_PROOF CVC4_STATISTICS_ON CVC4_USE_CRYPTOMINISAT CXXFLAGS : -O2 -pipe -fstack-protector-strong -fno-strict-aliasing -O3 -Wall -Wno-deprecated -Wsuggest-override -Wnon-virtual-dtor -pthread -pthread CFLAGS : -O2 -pipe -fstack-protector-strong -fno-strict-aliasing -O3 -Wall -fexceptions -Wno-deprecated -pthread -pthread Install prefix : /usr/local CVC4 license : GPLv3 (due to optional libraries; see below) Please note that CVC4 will be built against the following GPLed libraries: readline As these libraries are covered under the GPLv3, so is this build of CVC4. CVC4 is also available to you under the terms of the (modified) BSD license. If you prefer to license CVC4 under those terms, please configure CVC4 to disable all optional GPLed library dependencies (-DENABLE_BSD_ONLY=ON). Now just type make, followed by make check or make install. -- Configuring done -- Generating done CMake Warning (dev): Policy CMP0058 is not set: Ninja requires custom command byproducts to be explicit. Run "cmake --help-policy CMP0058" for policy details. Use the cmake_policy command to set the policy and suppress this warning. This project specifies custom command DEPENDS on files in the build tree that are not specified as the OUTPUT or BYPRODUCTS of any add_custom_command or add_custom_target: src/base/Debug_tags.tmp src/base/Trace_tags.tmp src/bindings/java/ArrayStoreAll.java src/bindings/java/ArrayStoreAllHashFunction.java src/bindings/java/ArrayType.java src/bindings/java/AscriptionType.java src/bindings/java/AscriptionTypeHashFunction.java src/bindings/java/AssertCommand.java src/bindings/java/BenchmarkStatus.java src/bindings/java/BitVector.java For compatibility with versions of CMake that did not have the BYPRODUCTS option, CMake is generating phony rules for such files to convince 'ninja' to build. Project authors should add the missing BYPRODUCTS or OUTPUT options to the custom commands that produce these files. This warning is for project developers. Use -Wno-dev to suppress it. CMake Warning: Manually-specified variables were not used by the project: CMAKE_COLOR_MAKEFILE CMAKE_CXX_FLAGS_DEBUG CMAKE_CXX_FLAGS_RELEASE CMAKE_C_FLAGS_DEBUG CMAKE_C_FLAGS_RELEASE CMAKE_VERBOSE_MAKEFILE -- Build files have been written to: /wrkdirs/usr/ports/math/cvc4/work/.build =========================================================================== =================================================== ===> Building for cvc4-1.7_6 [ 0% 2/465] cd /wrkdirs/usr/ports/math/cvc4/work/.build/src/base && /usr/local/bin/cmake -DGIT_FOUND=FALSE -P GitInfo.cmake [ 0% 3/465] cd /wrkdirs/usr/ports/math/cvc4/work/.build/src/base && /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/gentmptags.sh /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base Debug /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/api/cvc4cpp.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/api/cvc4cpp.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/api/cvc4cppkind.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/configuration.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/configuration.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/configuration_private.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/cvc4_assert.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/cvc4_assert.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/cvc4_check.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/cvc4_check.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/exception.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/excepti on.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/listener.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/listener.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/map_util.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/modal_exception.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/output.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/output.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/bindings/java_iterator_adapter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/bindings/java_stream_adapters.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/bindings/swig.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/backtrackable.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cddense_set.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdhashmap.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdhashmap_forward.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdhashset.h\ /wrkdirs/usr/ports/ma th/cvc4/work/CVC4-1.7/src/context/cdhashset_! forward.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdinsert_hashmap.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdinsert_hashmap_forward.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdlist.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdlist_forward.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdmaybe.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdo.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdqueue.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdtrail_queue.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/context.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/context.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/context_mm.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/context_mm.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/decision/decision_attributes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/decision/decision_engine .cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/decision/decision_engine.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/decision/decision_strategy.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/decision/justification_heuristic.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/decision/justification_heuristic.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/array.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/array_store_all.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/array_store_all.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/ascription_type.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/attribute.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/attribute.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/attribute_internals.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/attribute_unique_id.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/chain.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/ datatype.cpp\ /wrkdirs/usr/ports/math/cvc4/w! ork/CVC4-! 1.7/src/expr/datatype.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/emptyset.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/emptyset.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/expr_iomanip.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/expr_iomanip.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/expr_manager_scope.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/expr_manager_template.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/expr_manager_template.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/expr_stream.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/expr_template.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/expr_template.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/kind_map.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/kind_template.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/kind_template.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/matcher.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/metakind_template.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/metakind_template.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_algorithm.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_algorithm.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_builder.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_manager.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_manager.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_manager_attributes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_manager_listeners.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_manager_listeners.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_self_iterator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_trie.cpp\ / wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/sr! c/expr/no! de_trie.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_value.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_value.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/pickle_data.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/pickle_data.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/pickler.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/pickler.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/record.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/record.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/symbol_table.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/symbol_table.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/type.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/type.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/type_checker.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/type_checker_template.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/typ e_node.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/type_node.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/type_properties_template.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/uninterpreted_constant.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/uninterpreted_constant.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/variable_type_map.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/include/cvc4.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/include/cvc4_private.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/include/cvc4_private_library.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/include/cvc4_public.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/include/cvc4parser_private.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/include/cvc4parser_public.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/lib/clock_gettime.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/lib/ffs.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/ lib/replacements.h\ /wrkdirs/usr/ports/math/! cvc4/work! /CVC4-1.7/src/lib/strtok_r.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/command_executor.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/command_executor.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/command_executor_portfolio.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/command_executor_portfolio.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/driver_unified.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/interactive_shell.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/interactive_shell.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/main.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/main.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/portfolio.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/portfolio.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/portfolio_util.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/portfolio_util.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4- 1.7/src/main/util.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/argument_extender.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/argument_extender_implementation.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/argument_extender_implementation.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/arith_heuristic_pivot_rule.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/arith_heuristic_pivot_rule.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/arith_propagation_mode.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/arith_propagation_mode.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/arith_unate_lemma_mode.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/arith_unate_lemma_mode.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/base_handlers.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/bool_to_bv_mode.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/bool_to_bv_ mode.h\ /wrkdirs/usr/ports/math/cvc4/work/CV! C4-1.7/sr! c/options/bv_bitblast_mode.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/bv_bitblast_mode.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/datatypes_modes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/decision_mode.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/decision_mode.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/decision_weight.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/didyoumean.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/didyoumean.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/didyoumean_test.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/language.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/language.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/module_template.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/module_template.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/open_ostream.cpp\ /wrkdirs/usr/ports/ma th/cvc4/work/CVC4-1.7/src/options/open_ostream.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/option_exception.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/option_exception.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/options.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/options_handler.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/options_handler.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/options_holder_template.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/options_public_functions.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/options_template.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/printer_modes.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/printer_modes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/quantifiers_modes.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/quantifiers_modes.h\ /wrkdirs/usr/ports/math/cvc4/work/C VC4-1.7/src/options/set_language.cpp\ /wrkdi! rs/usr/po! rts/math/cvc4/work/CVC4-1.7/src/options/set_language.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/smt_modes.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/smt_modes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/strings_process_loop_mode.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/strings_process_loop_mode.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/sygus_out_mode.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/theoryof_mode.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/theoryof_mode.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/ufss_mode.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/antlr_input.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/antlr_input.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/antlr_input_imports.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/antlr_line_buffered_input.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7 /src/parser/antlr_line_buffered_input.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/antlr_tracing.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/bounded_token_buffer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/bounded_token_buffer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/bounded_token_factory.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/bounded_token_factory.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/cvc/Cvc.g\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/cvc/cvc_input.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/cvc/cvc_input.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/input.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/input.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/line_buffer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/line_buffer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/memory_mapped_input_buffer.cpp\ /wrk dirs/usr/ports/math/cvc4/work/CVC4-1.7/src/p! arser/mem! ory_mapped_input_buffer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/parser.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/parser.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/parser_builder.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/parser_builder.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/parser_exception.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt1/Smt1.g\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt1/smt1.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt1/smt1.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt1/smt1_input.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt1/smt1_input.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt2/Smt2.g\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt2/smt2.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt2/smt2.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt2/smt2_in put.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt2/smt2_input.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt2/sygus_input.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt2/sygus_input.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/tptp/Tptp.g\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/tptp/tptp.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/tptp/tptp.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/tptp/tptp_input.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/tptp/tptp_input.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/assertion_pipeline.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/assertion_pipeline.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/apply_substs.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/apply_substs.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/apply_to _const.cpp\ /wrkdirs/usr/ports/math/cvc4/wor! k/CVC4-1.! 7/src/preprocessing/passes/apply_to_const.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bool_to_bv.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bool_to_bv.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_abstraction.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_abstraction.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_ackermann.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_ackermann.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_eager_atoms.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_eager_atoms.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_gauss.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_gauss.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_intro_pow2.cpp\ /wrkdirs/usr/ports/ math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_intro_pow2.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_to_bool.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_to_bool.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/extended_rewriter_pass.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/extended_rewriter_pass.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/global_negate.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/global_negate.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/int_to_bv.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/int_to_bv.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/ite_removal.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/ite_removal.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/ite _simp.cpp\ /wrkdirs/usr/ports/math/cvc4/work! /CVC4-1.7! /src/preprocessing/passes/ite_simp.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/miplib_trick.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/miplib_trick.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/nl_ext_purify.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/nl_ext_purify.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/non_clausal_simp.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/non_clausal_simp.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/pseudo_boolean_processor.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/pseudo_boolean_processor.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/quantifier_macros.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/quantifier_macros.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/pass es/quantifiers_preprocess.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/quantifiers_preprocess.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/real_to_int.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/real_to_int.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/rewrite.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/rewrite.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/sep_skolem_emp.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/sep_skolem_emp.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/sort_infer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/sort_infer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/static_learning.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/static_learning.h\ /wrkdirs/usr/ports/math/cvc4 /work/CVC4-1.7/src/preprocessing/passes/sygu! s_abduct.! cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/sygus_abduct.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/sygus_inference.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/sygus_inference.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/symmetry_breaker.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/symmetry_breaker.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/symmetry_detect.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/symmetry_detect.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/synth_rew_rules.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/synth_rew_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/theory_preprocess.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/theory_preprocess.h\ /wrkdirs/usr/ports/mat h/cvc4/work/CVC4-1.7/src/preprocessing/passes/unconstrained_simplifier.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/unconstrained_simplifier.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/preprocessing_pass.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/preprocessing_pass.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/preprocessing_pass_context.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/preprocessing_pass_context.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/preprocessing_pass_registry.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/preprocessing_pass_registry.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/util/ite_utilities.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/util/ite_utilities.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/ast/ast_printer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/ src/printer/ast/ast_printer.h\ /wrkdirs/usr/! ports/mat! h/cvc4/work/CVC4-1.7/src/printer/cvc/cvc_printer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/cvc/cvc_printer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/dagification_visitor.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/dagification_visitor.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/printer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/printer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/smt2/smt2_printer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/smt2/smt2_printer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/sygus_print_callback.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/sygus_print_callback.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/tptp/tptp_printer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/tptp/tptp_printer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/arith_proof.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC 4-1.7/src/proof/arith_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/arith_proof_recorder.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/arith_proof_recorder.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/array_proof.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/array_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/bitvector_proof.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/bitvector_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/clausal_bitvector_proof.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/clausal_bitvector_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/clause_id.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/cnf_proof.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/cnf_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/dimacs_printer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/dimacs_printer.h\ /wrkdirs/usr/ports/m ath/cvc4/work/CVC4-1.7/src/proof/drat/drat_p! roof.cpp\! /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/drat/drat_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/er/er_proof.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/er/er_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/lemma_proof.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/lemma_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/lfsc_proof_printer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/lfsc_proof_printer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/lrat/lrat_proof.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/lrat/lrat_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/proof_manager.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/proof_manager.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/proof_output_channel.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/proof_output_c hannel.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/proof_utils.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/proof_utils.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/resolution_bitvector_proof.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/resolution_bitvector_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/sat_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/sat_proof_implementation.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/simplify_boolean_node.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/simplify_boolean_node.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/skolemization_manager.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/skolemization_manager.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/theory_proof.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/theory_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/uf_proof.cpp\ /wrkdirs/us r/ports/math/cvc4/work/CVC4-1.7/src/proof/uf! _proof.h\! /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/unsat_core.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/unsat_core.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bv_sat_solver_notify.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/bvminisat.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/bvminisat.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/core/Dimacs.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/core/Main.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/core/Solver.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/core/Solver.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/core/SolverTypes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/mtl/Alg.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/mtl/Alloc.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/mtl/Heap.h\ /wrkdirs/usr/ports/m ath/cvc4/work/CVC4-1.7/src/prop/bvminisat/mtl/IntTypes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/mtl/Map.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/mtl/Queue.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/mtl/Sort.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/mtl/Vec.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/mtl/XAlloc.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/simp/Main.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/simp/SimpSolver.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/simp/SimpSolver.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/utils/Options.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/utils/Options.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/utils/ParseUtils.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/utils/System.cc\ /wrkdirs/ usr/ports/math/cvc4/work/CVC4-1.7/src/prop/b! vminisat/! utils/System.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/cadical.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/cadical.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/cnf_stream.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/cnf_stream.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/cryptominisat.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/cryptominisat.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/core/Dimacs.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/core/Main.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/core/Solver.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/core/Solver.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/core/SolverTypes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/minisat.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/minisat.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/min isat/mtl/Alg.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/mtl/Alloc.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/mtl/Heap.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/mtl/IntTypes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/mtl/Map.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/mtl/Queue.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/mtl/Sort.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/mtl/Vec.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/mtl/XAlloc.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/simp/Main.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/simp/SimpSolver.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/simp/SimpSolver.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/utils/Options.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/utils/Options.h\ /wrkdirs/us r/ports/math/cvc4/work/CVC4-1.7/src/prop/min! isat/util! s/ParseUtils.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/utils/System.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/utils/System.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/prop_engine.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/prop_engine.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/registrar.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/sat_solver.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/sat_solver_factory.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/sat_solver_factory.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/sat_solver_types.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/theory_proxy.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/theory_proxy.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/command.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/command.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/command_list.cpp\ /wrkdi rs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/command_list.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/dump.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/dump.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/logic_exception.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/logic_request.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/logic_request.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/managed_ostreams.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/managed_ostreams.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/model.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/model.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/model_core_builder.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/model_core_builder.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/smt_engine.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/smt_engine.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/smt_engine_ scope.cpp\ /wrkdirs/usr/ports/math/cvc4/work! /CVC4-1.7! /src/smt/smt_engine_scope.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/smt_statistics_registry.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/smt_statistics_registry.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/term_formula_removal.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/term_formula_removal.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/update_ostream.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt_util/boolean_simplification.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt_util/boolean_simplification.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt_util/lemma_channels.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt_util/lemma_channels.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt_util/lemma_input_channel.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt_util/lemma_output_channel.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt_util/nary_builder.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1 .7/src/smt_util/nary_builder.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt_util/node_visitor.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/approx_simplex.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/approx_simplex.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arith_ite_utils.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arith_ite_utils.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arith_msum.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arith_msum.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arith_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arith_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arith_static_learner.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arith_static_learner.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arith_utilities.h\ /wrkdirs/usr/ports /math/cvc4/work/CVC4-1.7/src/theory/arith/ar! ithvar.cp! p\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arithvar.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arithvar_node_map.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/attempt_solution_simplex.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/attempt_solution_simplex.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/bound_counts.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/callbacks.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/callbacks.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/congruence_manager.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/congruence_manager.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/constraint.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/constraint.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/constraint_forward.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1. 7/src/theory/arith/cut_log.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/cut_log.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/delta_rational.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/delta_rational.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/dio_solver.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/dio_solver.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/dual_simplex.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/dual_simplex.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/error_set.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/error_set.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/fc_simplex.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/fc_simplex.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/infer_bounds.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/ar ith/infer_bounds.h\ /wrkdirs/usr/ports/math/! cvc4/work! /CVC4-1.7/src/theory/arith/linear_equality.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/linear_equality.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/matrix.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/matrix.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/nonlinear_extension.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/nonlinear_extension.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/normal_form.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/normal_form.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/partial_model.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/partial_model.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/simplex.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/simplex.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/simplex_update.cpp\ /wrkdirs/usr/ports/math/cvc4 /work/CVC4-1.7/src/theory/arith/simplex_update.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/soi_simplex.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/soi_simplex.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/tableau.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/tableau.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/tableau_sizes.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/tableau_sizes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/theory_arith.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/theory_arith.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/theory_arith_private.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/theory_arith_private.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/theory_arith_private_forward.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/theory_arith_type_r ules.h\ /wrkdirs/usr/ports/math/cvc4/work/CV! C4-1.7/sr! c/theory/arith/type_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/array_info.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/array_info.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/array_proof_reconstruction.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/array_proof_reconstruction.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/static_fact_manager.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/static_fact_manager.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/theory_arrays.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/theory_arrays.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/theory_arrays_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/theory_arrays_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/theory_arrays_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/ CVC4-1.7/src/theory/arrays/type_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/union_find.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/union_find.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/assertion.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/assertion.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/atom_requests.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/atom_requests.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/booleans/circuit_propagator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/booleans/circuit_propagator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/booleans/theory_bool.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/booleans/theory_bool.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/booleans/theory_bool_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/booleans/theory_bool_rewriter.h\ /wrkdirs/usr/ ports/math/cvc4/work/CVC4-1.7/src/theory/boo! leans/the! ory_bool_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/booleans/type_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/theory_builtin.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/theory_builtin.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/theory_builtin_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/theory_builtin_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/theory_builtin_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/type_enumerator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/type_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/abstraction.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/abstraction.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bitblast/aig_bitblaster.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bitbla st/aig_bitblaster.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bitblast/bitblast_strategies_template.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bitblast/bitblast_utils.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bitblast/bitblaster.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bitblast/eager_bitblaster.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bitblast/eager_bitblaster.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bitblast/lazy_bitblaster.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bitblast/lazy_bitblaster.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_eager_solver.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_eager_solver.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_inequality_graph.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_inequality_graph.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theor y/bv/bv_quick_check.cpp\ /wrkdirs/usr/ports/! math/cvc4! /work/CVC4-1.7/src/theory/bv/bv_quick_check.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_subtheory.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_subtheory_algebraic.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_subtheory_algebraic.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_subtheory_bitblast.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_subtheory_bitblast.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_subtheory_core.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_subtheory_core.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_subtheory_inequality.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_subtheory_inequality.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/slicer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/slicer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv.cpp\ /wrkdir s/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules_core.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules_normalization.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules_simplification.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv_utils.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CV C4-1.7/src/theory/bv/theory_bv_utils.h\ /wrk! dirs/usr/! ports/math/cvc4/work/CVC4-1.7/src/theory/bv/type_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/care_graph.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/datatypes_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/datatypes_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/datatypes_sygus.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/datatypes_sygus.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/sygus_simple_sym.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/sygus_simple_sym.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/theory_datatypes.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/theory_datatypes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/theory_datatypes_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/type_enumerator.cpp\ /wrk dirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/type_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/decision_manager.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/decision_manager.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/decision_strategy.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/decision_strategy.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/evaluator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/evaluator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/example/ecdata.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/example/ecdata.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/example/theory_uf_tim.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/example/theory_uf_tim.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/ext_theory.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/ext_theory.h\ /wrkdirs/usr/ports/math/cvc4/work/CV C4-1.7/src/theory/fp/fp_converter.cpp\ /wrkd! irs/usr/p! orts/math/cvc4/work/CVC4-1.7/src/theory/fp/fp_converter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/fp/theory_fp.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/fp/theory_fp.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/fp/theory_fp_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/fp/theory_fp_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/fp/theory_fp_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/fp/type_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/idl_assertion.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/idl_assertion.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/idl_assertion_db.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/idl_assertion_db.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/idl_model.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/idl_model.h\ /wrkdirs/usr/ports/math/c vc4/work/CVC4-1.7/src/theory/idl/theory_idl.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/theory_idl.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/interrupted.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/logic_info.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/logic_info.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/output_channel.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/alpha_equivalence.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/alpha_equivalence.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/anti_skolem.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/anti_skolem.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/bv_inverter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/bv_inverter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/bv_inverter_utils.cpp\ /wrk dirs/usr/ports/math/cvc4/work/CVC4-1.7/src/t! heory/qua! ntifiers/bv_inverter_utils.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/candidate_rewrite_database.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/candidate_rewrite_database.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/candidate_rewrite_filter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/candidate_rewrite_filter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_bv_instantiato r_utils.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_instantiator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_instantiator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/conjecture_generator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/conjecture_generator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1 .7/src/theory/quantifiers/dynamic_rewrite.cp! p\ /wrkdi! rs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/dynamic_rewrite.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/candidate_generator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/candidate_generator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/ho_trigger.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/ho_trigger.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/inst_match_generator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/inst_match_generator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/inst_strategy_e_matching.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/instantiation_engine.cpp\ /wrkdirs/usr/ports/mat h/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/instantiation_engine.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/trigger.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/trigger.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/equality_infer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/equality_infer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/equality_query.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/equality_query.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/expr_miner.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/expr_miner.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/expr_miner_manager.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/expr_miner_manager.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifie rs/extended_rewrite.cpp\ /wrkdirs/usr/ports/! math/cvc4! /work/CVC4-1.7/src/theory/quantifiers/extended_rewrite.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/first_order_model.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/first_order_model.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/fmf/bounded_integers.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/fmf/bounded_integers.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/fmf/full_model_check.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/fmf/full_model_check.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/fmf/model_builder.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/fmf/model_builder.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/fmf/model_engine.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/fmf/model_engine.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/th eory/quantifiers/fun_def_process.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/fun_def_process.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/inst_match.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/inst_match.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/inst_match_trie.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/inst_match_trie.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/inst_propagator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/inst_propagator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/inst_strategy_enumerative.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/inst_strategy_enumerative.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/instantiate.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/instantiate.h\ /wrkdirs/usr /ports/math/cvc4/work/CVC4-1.7/src/theory/qu! antifiers! /lazy_trie.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/lazy_trie.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/local_theory_ext.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/local_theory_ext.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quant_conflict_find.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quant_conflict_find.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quant_epr.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quant_epr.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quant_relevance.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quant_relevance.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quant_split.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quant_split.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theor y/quantifiers/quant_util.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quant_util.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quantifiers_attributes.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quantifiers_attributes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quantifiers_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quantifiers_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/query_generator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/query_generator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/relevant_domain.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/relevant_domain.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/rewrite_engine.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/rewrite_engine.h\ /wrkd irs/usr/ports/math/cvc4/work/CVC4-1.7/src/th! eory/quan! tifiers/single_inv_partition.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/single_inv_partition.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/skolemize.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/skolemize.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/solution_filter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/solution_filter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/ce_guided_single_inv.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/cegis.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifi ers/sygus/cegis.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/cegis_unif.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/cegis_unif.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/enum_stream_substitution.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/enum_stream_substitution.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_enumerator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_eval_unfold.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_explain.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_explain.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/t heory/quantifiers/sygus/sygus_grammar_cons.c! pp\ /wrkd! irs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_cons.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_norm.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_red.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_red.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_invariance.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_invariance.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_module.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_module.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_pbe.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_p be.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_process_conj.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_process_conj.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_repair_const.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_repair_const.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif_io.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif_io.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif_rl.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif_rl.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus _unif_strat.cpp\ /wrkdirs/usr/ports/math/cvc! 4/work/CV! C4-1.7/src/theory/quantifiers/sygus/sygus_unif_strat.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/synth_conjecture.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/synth_conjecture.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/synth_engine.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/synth_engine.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/term_database_sygus.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/term_database_sygus.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus_sampler.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus_sampler.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/term_canonize.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/term_canonize.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/th eory/quantifiers/term_database.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/term_database.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/term_enumeration.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/term_enumeration.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/term_util.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/term_util.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/theory_quantifiers.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/theory_quantifiers.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/theory_quantifiers_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers_engine.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers_engine.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/rep_set.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src /theory/rep_set.h\ /wrkdirs/usr/ports/math/c! vc4/work/! CVC4-1.7/src/theory/rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/rewriter_attributes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/rewriter_tables_template.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sep/theory_sep.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sep/theory_sep.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sep/theory_sep_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sep/theory_sep_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sep/theory_sep_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/normal_form.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/rels_utils.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/theory_sets.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/theory_sets.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/t heory/sets/theory_sets_private.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/theory_sets_private.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/theory_sets_rels.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/theory_sets_rels.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/theory_sets_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/theory_sets_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/theory_sets_type_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/theory_sets_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/shared_terms_database.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/shared_terms_database.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sort_inference.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sort_inference.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/regexp_e lim.cpp\ /wrkdirs/usr/ports/math/cvc4/work/C! VC4-1.7/s! rc/theory/strings/regexp_elim.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/regexp_operation.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/regexp_operation.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/regexp_solver.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/regexp_solver.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/skolem_cache.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/skolem_cache.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/theory_strings.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/theory_strings.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/theory_strings_preprocess.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/theory_strings_preprocess.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/theory_strings_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/ src/theory/strings/theory_strings_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/theory_strings_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/type_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/subs_minimize.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/subs_minimize.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/substitutions.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/substitutions.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/term_registration_visitor.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/term_registration_visitor.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/theory.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/theory.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/theory_engine.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/theory_engine.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/th eory/theory_model.cpp\ /wrkdirs/usr/ports/ma! th/cvc4/w! ork/CVC4-1.7/src/theory/theory_model.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/theory_model_builder.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/theory_model_builder.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/theory_registrar.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/theory_test_utils.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/theory_traits_template.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/type_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/type_enumerator_template.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/type_set.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/type_set.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/equality_engine.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/equality_engine.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/equality_engine_types.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/ src/theory/uf/symmetry_breaker.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/symmetry_breaker.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/theory_uf.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/theory_uf.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/theory_uf_model.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/theory_uf_model.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/theory_uf_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/theory_uf_strong_solver.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/theory_uf_strong_solver.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/theory_uf_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/valuation.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/valuation.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/abstract_value.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/uti l/abstract_value.h\ /wrkdirs/usr/ports/math/! cvc4/work! /CVC4-1.7/src/util/bin_heap.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/bitvector.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/bitvector.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/bool.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/cardinality.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/cardinality.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/channel.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/debug.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/dense_map.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/divisible.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/divisible.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/floatingpoint.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/gmp_util.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/hash.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/index.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/index.h \ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/integer_cln_imp.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/integer_cln_imp.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/integer_gmp_imp.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/integer_gmp_imp.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/maybe.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/ostream_util.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/ostream_util.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/random.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/random.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/rational_cln_imp.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/rational_cln_imp.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/rational_gmp_imp.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/rational_gmp_imp.h\ /wrkdirs/usr/ports/math/cvc4/ work/CVC4-1.7/src/util/regexp.cpp\ /wrkdirs/! usr/ports! /math/cvc4/work/CVC4-1.7/src/util/regexp.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/resource_manager.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/resource_manager.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/result.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/result.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/safe_print.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/safe_print.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/sampler.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/sampler.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/sexpr.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/sexpr.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/smt2_quote_string.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/smt2_quote_string.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/statistics.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/statistics.h\ /wrkdirs/usr/ ports/math/cvc4/work/CVC4-1.7/src/util/statistics_registry.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/statistics_registry.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/tuple.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/unsafe_interrupt_exception.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/utility.h [ 0% 4/465] cd /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr && /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/mkkind /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/kind_template.h /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/booleans/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/fp/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sep/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/kinds /wrk dirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/kinds > /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr/kind.h [ 0% 5/465] cd /wrkdirs/usr/ports/math/cvc4/work/.build/src/base && /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/gentmptags.sh /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base Trace /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/api/cvc4cpp.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/api/cvc4cpp.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/api/cvc4cppkind.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/configuration.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/configuration.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/configuration_private.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/cvc4_assert.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/cvc4_assert.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/cvc4_check.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/cvc4_check.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/exception.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/excepti on.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/listener.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/listener.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/map_util.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/modal_exception.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/output.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/output.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/bindings/java_iterator_adapter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/bindings/java_stream_adapters.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/bindings/swig.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/backtrackable.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cddense_set.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdhashmap.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdhashmap_forward.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdhashset.h\ /wrkdirs/usr/ports/ma th/cvc4/work/CVC4-1.7/src/context/cdhashset_! forward.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdinsert_hashmap.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdinsert_hashmap_forward.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdlist.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdlist_forward.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdmaybe.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdo.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdqueue.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/cdtrail_queue.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/context.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/context.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/context_mm.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/context/context_mm.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/decision/decision_attributes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/decision/decision_engine .cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/decision/decision_engine.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/decision/decision_strategy.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/decision/justification_heuristic.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/decision/justification_heuristic.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/array.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/array_store_all.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/array_store_all.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/ascription_type.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/attribute.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/attribute.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/attribute_internals.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/attribute_unique_id.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/chain.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/ datatype.cpp\ /wrkdirs/usr/ports/math/cvc4/w! ork/CVC4-! 1.7/src/expr/datatype.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/emptyset.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/emptyset.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/expr_iomanip.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/expr_iomanip.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/expr_manager_scope.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/expr_manager_template.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/expr_manager_template.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/expr_stream.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/expr_template.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/expr_template.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/kind_map.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/kind_template.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/kind_template.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/matcher.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/metakind_template.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/metakind_template.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_algorithm.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_algorithm.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_builder.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_manager.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_manager.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_manager_attributes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_manager_listeners.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_manager_listeners.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_self_iterator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_trie.cpp\ / wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/sr! c/expr/no! de_trie.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_value.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/node_value.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/pickle_data.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/pickle_data.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/pickler.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/pickler.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/record.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/record.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/symbol_table.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/symbol_table.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/type.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/type.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/type_checker.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/type_checker_template.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/typ e_node.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/type_node.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/type_properties_template.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/uninterpreted_constant.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/uninterpreted_constant.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/variable_type_map.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/include/cvc4.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/include/cvc4_private.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/include/cvc4_private_library.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/include/cvc4_public.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/include/cvc4parser_private.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/include/cvc4parser_public.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/lib/clock_gettime.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/lib/ffs.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/ lib/replacements.h\ /wrkdirs/usr/ports/math/! cvc4/work! /CVC4-1.7/src/lib/strtok_r.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/command_executor.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/command_executor.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/command_executor_portfolio.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/command_executor_portfolio.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/driver_unified.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/interactive_shell.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/interactive_shell.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/main.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/main.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/portfolio.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/portfolio.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/portfolio_util.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/main/portfolio_util.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4- 1.7/src/main/util.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/argument_extender.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/argument_extender_implementation.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/argument_extender_implementation.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/arith_heuristic_pivot_rule.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/arith_heuristic_pivot_rule.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/arith_propagation_mode.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/arith_propagation_mode.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/arith_unate_lemma_mode.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/arith_unate_lemma_mode.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/base_handlers.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/bool_to_bv_mode.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/bool_to_bv_ mode.h\ /wrkdirs/usr/ports/math/cvc4/work/CV! C4-1.7/sr! c/options/bv_bitblast_mode.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/bv_bitblast_mode.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/datatypes_modes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/decision_mode.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/decision_mode.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/decision_weight.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/didyoumean.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/didyoumean.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/didyoumean_test.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/language.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/language.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/module_template.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/module_template.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/open_ostream.cpp\ /wrkdirs/usr/ports/ma th/cvc4/work/CVC4-1.7/src/options/open_ostream.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/option_exception.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/option_exception.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/options.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/options_handler.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/options_handler.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/options_holder_template.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/options_public_functions.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/options_template.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/printer_modes.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/printer_modes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/quantifiers_modes.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/quantifiers_modes.h\ /wrkdirs/usr/ports/math/cvc4/work/C VC4-1.7/src/options/set_language.cpp\ /wrkdi! rs/usr/po! rts/math/cvc4/work/CVC4-1.7/src/options/set_language.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/smt_modes.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/smt_modes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/strings_process_loop_mode.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/strings_process_loop_mode.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/sygus_out_mode.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/theoryof_mode.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/theoryof_mode.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/options/ufss_mode.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/antlr_input.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/antlr_input.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/antlr_input_imports.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/antlr_line_buffered_input.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7 /src/parser/antlr_line_buffered_input.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/antlr_tracing.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/bounded_token_buffer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/bounded_token_buffer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/bounded_token_factory.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/bounded_token_factory.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/cvc/Cvc.g\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/cvc/cvc_input.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/cvc/cvc_input.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/input.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/input.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/line_buffer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/line_buffer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/memory_mapped_input_buffer.cpp\ /wrk dirs/usr/ports/math/cvc4/work/CVC4-1.7/src/p! arser/mem! ory_mapped_input_buffer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/parser.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/parser.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/parser_builder.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/parser_builder.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/parser_exception.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt1/Smt1.g\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt1/smt1.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt1/smt1.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt1/smt1_input.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt1/smt1_input.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt2/Smt2.g\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt2/smt2.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt2/smt2.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt2/smt2_in put.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt2/smt2_input.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt2/sygus_input.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/smt2/sygus_input.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/tptp/Tptp.g\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/tptp/tptp.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/tptp/tptp.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/tptp/tptp_input.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/parser/tptp/tptp_input.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/assertion_pipeline.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/assertion_pipeline.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/apply_substs.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/apply_substs.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/apply_to _const.cpp\ /wrkdirs/usr/ports/math/cvc4/wor! k/CVC4-1.! 7/src/preprocessing/passes/apply_to_const.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bool_to_bv.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bool_to_bv.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_abstraction.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_abstraction.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_ackermann.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_ackermann.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_eager_atoms.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_eager_atoms.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_gauss.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_gauss.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_intro_pow2.cpp\ /wrkdirs/usr/ports/ math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_intro_pow2.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_to_bool.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/bv_to_bool.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/extended_rewriter_pass.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/extended_rewriter_pass.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/global_negate.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/global_negate.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/int_to_bv.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/int_to_bv.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/ite_removal.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/ite_removal.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/ite _simp.cpp\ /wrkdirs/usr/ports/math/cvc4/work! /CVC4-1.7! /src/preprocessing/passes/ite_simp.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/miplib_trick.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/miplib_trick.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/nl_ext_purify.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/nl_ext_purify.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/non_clausal_simp.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/non_clausal_simp.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/pseudo_boolean_processor.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/pseudo_boolean_processor.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/quantifier_macros.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/quantifier_macros.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/pass es/quantifiers_preprocess.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/quantifiers_preprocess.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/real_to_int.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/real_to_int.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/rewrite.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/rewrite.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/sep_skolem_emp.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/sep_skolem_emp.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/sort_infer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/sort_infer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/static_learning.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/static_learning.h\ /wrkdirs/usr/ports/math/cvc4 /work/CVC4-1.7/src/preprocessing/passes/sygu! s_abduct.! cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/sygus_abduct.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/sygus_inference.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/sygus_inference.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/symmetry_breaker.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/symmetry_breaker.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/symmetry_detect.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/symmetry_detect.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/synth_rew_rules.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/synth_rew_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/theory_preprocess.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/theory_preprocess.h\ /wrkdirs/usr/ports/mat h/cvc4/work/CVC4-1.7/src/preprocessing/passes/unconstrained_simplifier.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/passes/unconstrained_simplifier.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/preprocessing_pass.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/preprocessing_pass.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/preprocessing_pass_context.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/preprocessing_pass_context.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/preprocessing_pass_registry.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/preprocessing_pass_registry.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/util/ite_utilities.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/preprocessing/util/ite_utilities.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/ast/ast_printer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/ src/printer/ast/ast_printer.h\ /wrkdirs/usr/! ports/mat! h/cvc4/work/CVC4-1.7/src/printer/cvc/cvc_printer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/cvc/cvc_printer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/dagification_visitor.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/dagification_visitor.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/printer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/printer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/smt2/smt2_printer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/smt2/smt2_printer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/sygus_print_callback.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/sygus_print_callback.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/tptp/tptp_printer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/printer/tptp/tptp_printer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/arith_proof.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC 4-1.7/src/proof/arith_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/arith_proof_recorder.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/arith_proof_recorder.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/array_proof.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/array_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/bitvector_proof.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/bitvector_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/clausal_bitvector_proof.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/clausal_bitvector_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/clause_id.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/cnf_proof.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/cnf_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/dimacs_printer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/dimacs_printer.h\ /wrkdirs/usr/ports/m ath/cvc4/work/CVC4-1.7/src/proof/drat/drat_p! roof.cpp\! /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/drat/drat_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/er/er_proof.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/er/er_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/lemma_proof.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/lemma_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/lfsc_proof_printer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/lfsc_proof_printer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/lrat/lrat_proof.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/lrat/lrat_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/proof_manager.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/proof_manager.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/proof_output_channel.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/proof_output_c hannel.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/proof_utils.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/proof_utils.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/resolution_bitvector_proof.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/resolution_bitvector_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/sat_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/sat_proof_implementation.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/simplify_boolean_node.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/simplify_boolean_node.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/skolemization_manager.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/skolemization_manager.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/theory_proof.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/theory_proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/uf_proof.cpp\ /wrkdirs/us r/ports/math/cvc4/work/CVC4-1.7/src/proof/uf! _proof.h\! /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/unsat_core.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/proof/unsat_core.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bv_sat_solver_notify.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/bvminisat.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/bvminisat.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/core/Dimacs.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/core/Main.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/core/Solver.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/core/Solver.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/core/SolverTypes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/mtl/Alg.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/mtl/Alloc.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/mtl/Heap.h\ /wrkdirs/usr/ports/m ath/cvc4/work/CVC4-1.7/src/prop/bvminisat/mtl/IntTypes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/mtl/Map.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/mtl/Queue.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/mtl/Sort.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/mtl/Vec.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/mtl/XAlloc.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/simp/Main.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/simp/SimpSolver.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/simp/SimpSolver.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/utils/Options.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/utils/Options.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/utils/ParseUtils.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/bvminisat/utils/System.cc\ /wrkdirs/ usr/ports/math/cvc4/work/CVC4-1.7/src/prop/b! vminisat/! utils/System.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/cadical.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/cadical.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/cnf_stream.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/cnf_stream.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/cryptominisat.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/cryptominisat.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/core/Dimacs.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/core/Main.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/core/Solver.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/core/Solver.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/core/SolverTypes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/minisat.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/minisat.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/min isat/mtl/Alg.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/mtl/Alloc.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/mtl/Heap.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/mtl/IntTypes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/mtl/Map.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/mtl/Queue.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/mtl/Sort.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/mtl/Vec.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/mtl/XAlloc.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/simp/Main.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/simp/SimpSolver.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/simp/SimpSolver.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/utils/Options.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/utils/Options.h\ /wrkdirs/us r/ports/math/cvc4/work/CVC4-1.7/src/prop/min! isat/util! s/ParseUtils.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/utils/System.cc\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/minisat/utils/System.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/prop_engine.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/prop_engine.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/registrar.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/sat_solver.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/sat_solver_factory.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/sat_solver_factory.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/sat_solver_types.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/theory_proxy.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/prop/theory_proxy.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/command.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/command.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/command_list.cpp\ /wrkdi rs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/command_list.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/dump.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/dump.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/logic_exception.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/logic_request.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/logic_request.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/managed_ostreams.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/managed_ostreams.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/model.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/model.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/model_core_builder.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/model_core_builder.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/smt_engine.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/smt_engine.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/smt_engine_ scope.cpp\ /wrkdirs/usr/ports/math/cvc4/work! /CVC4-1.7! /src/smt/smt_engine_scope.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/smt_statistics_registry.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/smt_statistics_registry.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/term_formula_removal.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/term_formula_removal.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt/update_ostream.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt_util/boolean_simplification.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt_util/boolean_simplification.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt_util/lemma_channels.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt_util/lemma_channels.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt_util/lemma_input_channel.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt_util/lemma_output_channel.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt_util/nary_builder.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1 .7/src/smt_util/nary_builder.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/smt_util/node_visitor.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/approx_simplex.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/approx_simplex.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arith_ite_utils.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arith_ite_utils.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arith_msum.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arith_msum.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arith_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arith_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arith_static_learner.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arith_static_learner.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arith_utilities.h\ /wrkdirs/usr/ports /math/cvc4/work/CVC4-1.7/src/theory/arith/ar! ithvar.cp! p\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arithvar.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/arithvar_node_map.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/attempt_solution_simplex.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/attempt_solution_simplex.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/bound_counts.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/callbacks.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/callbacks.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/congruence_manager.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/congruence_manager.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/constraint.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/constraint.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/constraint_forward.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1. 7/src/theory/arith/cut_log.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/cut_log.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/delta_rational.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/delta_rational.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/dio_solver.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/dio_solver.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/dual_simplex.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/dual_simplex.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/error_set.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/error_set.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/fc_simplex.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/fc_simplex.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/infer_bounds.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/ar ith/infer_bounds.h\ /wrkdirs/usr/ports/math/! cvc4/work! /CVC4-1.7/src/theory/arith/linear_equality.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/linear_equality.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/matrix.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/matrix.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/nonlinear_extension.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/nonlinear_extension.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/normal_form.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/normal_form.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/partial_model.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/partial_model.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/simplex.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/simplex.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/simplex_update.cpp\ /wrkdirs/usr/ports/math/cvc4 /work/CVC4-1.7/src/theory/arith/simplex_update.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/soi_simplex.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/soi_simplex.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/tableau.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/tableau.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/tableau_sizes.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/tableau_sizes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/theory_arith.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/theory_arith.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/theory_arith_private.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/theory_arith_private.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/theory_arith_private_forward.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/theory_arith_type_r ules.h\ /wrkdirs/usr/ports/math/cvc4/work/CV! C4-1.7/sr! c/theory/arith/type_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/array_info.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/array_info.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/array_proof_reconstruction.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/array_proof_reconstruction.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/static_fact_manager.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/static_fact_manager.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/theory_arrays.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/theory_arrays.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/theory_arrays_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/theory_arrays_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/theory_arrays_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/ CVC4-1.7/src/theory/arrays/type_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/union_find.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/union_find.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/assertion.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/assertion.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/atom_requests.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/atom_requests.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/booleans/circuit_propagator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/booleans/circuit_propagator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/booleans/theory_bool.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/booleans/theory_bool.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/booleans/theory_bool_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/booleans/theory_bool_rewriter.h\ /wrkdirs/usr/ ports/math/cvc4/work/CVC4-1.7/src/theory/boo! leans/the! ory_bool_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/booleans/type_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/theory_builtin.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/theory_builtin.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/theory_builtin_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/theory_builtin_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/theory_builtin_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/type_enumerator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/type_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/abstraction.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/abstraction.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bitblast/aig_bitblaster.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bitbla st/aig_bitblaster.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bitblast/bitblast_strategies_template.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bitblast/bitblast_utils.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bitblast/bitblaster.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bitblast/eager_bitblaster.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bitblast/eager_bitblaster.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bitblast/lazy_bitblaster.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bitblast/lazy_bitblaster.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_eager_solver.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_eager_solver.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_inequality_graph.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_inequality_graph.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theor y/bv/bv_quick_check.cpp\ /wrkdirs/usr/ports/! math/cvc4! /work/CVC4-1.7/src/theory/bv/bv_quick_check.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_subtheory.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_subtheory_algebraic.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_subtheory_algebraic.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_subtheory_bitblast.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_subtheory_bitblast.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_subtheory_core.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_subtheory_core.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_subtheory_inequality.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/bv_subtheory_inequality.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/slicer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/slicer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv.cpp\ /wrkdir s/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules_core.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules_normalization.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules_simplification.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/theory_bv_utils.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CV C4-1.7/src/theory/bv/theory_bv_utils.h\ /wrk! dirs/usr/! ports/math/cvc4/work/CVC4-1.7/src/theory/bv/type_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/care_graph.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/datatypes_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/datatypes_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/datatypes_sygus.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/datatypes_sygus.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/sygus_simple_sym.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/sygus_simple_sym.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/theory_datatypes.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/theory_datatypes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/theory_datatypes_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/type_enumerator.cpp\ /wrk dirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/type_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/decision_manager.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/decision_manager.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/decision_strategy.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/decision_strategy.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/evaluator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/evaluator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/example/ecdata.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/example/ecdata.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/example/theory_uf_tim.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/example/theory_uf_tim.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/ext_theory.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/ext_theory.h\ /wrkdirs/usr/ports/math/cvc4/work/CV C4-1.7/src/theory/fp/fp_converter.cpp\ /wrkd! irs/usr/p! orts/math/cvc4/work/CVC4-1.7/src/theory/fp/fp_converter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/fp/theory_fp.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/fp/theory_fp.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/fp/theory_fp_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/fp/theory_fp_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/fp/theory_fp_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/fp/type_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/idl_assertion.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/idl_assertion.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/idl_assertion_db.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/idl_assertion_db.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/idl_model.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/idl_model.h\ /wrkdirs/usr/ports/math/c vc4/work/CVC4-1.7/src/theory/idl/theory_idl.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/theory_idl.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/interrupted.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/logic_info.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/logic_info.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/output_channel.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/alpha_equivalence.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/alpha_equivalence.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/anti_skolem.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/anti_skolem.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/bv_inverter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/bv_inverter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/bv_inverter_utils.cpp\ /wrk dirs/usr/ports/math/cvc4/work/CVC4-1.7/src/t! heory/qua! ntifiers/bv_inverter_utils.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/candidate_rewrite_database.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/candidate_rewrite_database.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/candidate_rewrite_filter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/candidate_rewrite_filter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_bv_instantiato r_utils.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_instantiator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_instantiator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/conjecture_generator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/conjecture_generator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1 .7/src/theory/quantifiers/dynamic_rewrite.cp! p\ /wrkdi! rs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/dynamic_rewrite.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/candidate_generator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/candidate_generator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/ho_trigger.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/ho_trigger.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/inst_match_generator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/inst_match_generator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/inst_strategy_e_matching.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/instantiation_engine.cpp\ /wrkdirs/usr/ports/mat h/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/instantiation_engine.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/trigger.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/ematching/trigger.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/equality_infer.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/equality_infer.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/equality_query.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/equality_query.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/expr_miner.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/expr_miner.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/expr_miner_manager.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/expr_miner_manager.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifie rs/extended_rewrite.cpp\ /wrkdirs/usr/ports/! math/cvc4! /work/CVC4-1.7/src/theory/quantifiers/extended_rewrite.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/first_order_model.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/first_order_model.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/fmf/bounded_integers.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/fmf/bounded_integers.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/fmf/full_model_check.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/fmf/full_model_check.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/fmf/model_builder.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/fmf/model_builder.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/fmf/model_engine.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/fmf/model_engine.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/th eory/quantifiers/fun_def_process.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/fun_def_process.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/inst_match.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/inst_match.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/inst_match_trie.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/inst_match_trie.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/inst_propagator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/inst_propagator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/inst_strategy_enumerative.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/inst_strategy_enumerative.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/instantiate.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/instantiate.h\ /wrkdirs/usr /ports/math/cvc4/work/CVC4-1.7/src/theory/qu! antifiers! /lazy_trie.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/lazy_trie.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/local_theory_ext.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/local_theory_ext.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quant_conflict_find.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quant_conflict_find.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quant_epr.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quant_epr.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quant_relevance.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quant_relevance.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quant_split.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quant_split.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theor y/quantifiers/quant_util.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quant_util.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quantifiers_attributes.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quantifiers_attributes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quantifiers_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/quantifiers_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/query_generator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/query_generator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/relevant_domain.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/relevant_domain.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/rewrite_engine.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/rewrite_engine.h\ /wrkd irs/usr/ports/math/cvc4/work/CVC4-1.7/src/th! eory/quan! tifiers/single_inv_partition.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/single_inv_partition.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/skolemize.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/skolemize.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/solution_filter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/solution_filter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/ce_guided_single_inv.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/cegis.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifi ers/sygus/cegis.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/cegis_unif.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/cegis_unif.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/enum_stream_substitution.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/enum_stream_substitution.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_enumerator.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_eval_unfold.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_explain.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_explain.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/t heory/quantifiers/sygus/sygus_grammar_cons.c! pp\ /wrkd! irs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_cons.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_norm.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_red.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_red.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_invariance.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_invariance.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_module.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_module.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_pbe.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_p be.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_process_conj.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_process_conj.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_repair_const.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_repair_const.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif_io.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif_io.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif_rl.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif_rl.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/sygus _unif_strat.cpp\ /wrkdirs/usr/ports/math/cvc! 4/work/CV! C4-1.7/src/theory/quantifiers/sygus/sygus_unif_strat.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/synth_conjecture.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/synth_conjecture.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/synth_engine.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/synth_engine.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/term_database_sygus.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus/term_database_sygus.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus_sampler.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/sygus_sampler.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/term_canonize.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/term_canonize.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/th eory/quantifiers/term_database.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/term_database.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/term_enumeration.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/term_enumeration.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/term_util.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/term_util.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/theory_quantifiers.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/theory_quantifiers.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/theory_quantifiers_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers_engine.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers_engine.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/rep_set.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src /theory/rep_set.h\ /wrkdirs/usr/ports/math/c! vc4/work/! CVC4-1.7/src/theory/rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/rewriter_attributes.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/rewriter_tables_template.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sep/theory_sep.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sep/theory_sep.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sep/theory_sep_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sep/theory_sep_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sep/theory_sep_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/normal_form.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/rels_utils.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/theory_sets.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/theory_sets.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/t heory/sets/theory_sets_private.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/theory_sets_private.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/theory_sets_rels.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/theory_sets_rels.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/theory_sets_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/theory_sets_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/theory_sets_type_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/theory_sets_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/shared_terms_database.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/shared_terms_database.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sort_inference.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sort_inference.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/regexp_e lim.cpp\ /wrkdirs/usr/ports/math/cvc4/work/C! VC4-1.7/s! rc/theory/strings/regexp_elim.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/regexp_operation.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/regexp_operation.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/regexp_solver.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/regexp_solver.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/skolem_cache.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/skolem_cache.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/theory_strings.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/theory_strings.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/theory_strings_preprocess.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/theory_strings_preprocess.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/theory_strings_rewriter.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/ src/theory/strings/theory_strings_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/theory_strings_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/type_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/subs_minimize.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/subs_minimize.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/substitutions.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/substitutions.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/term_registration_visitor.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/term_registration_visitor.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/theory.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/theory.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/theory_engine.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/theory_engine.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/th eory/theory_model.cpp\ /wrkdirs/usr/ports/ma! th/cvc4/w! ork/CVC4-1.7/src/theory/theory_model.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/theory_model_builder.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/theory_model_builder.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/theory_registrar.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/theory_test_utils.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/theory_traits_template.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/type_enumerator.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/type_enumerator_template.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/type_set.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/type_set.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/equality_engine.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/equality_engine.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/equality_engine_types.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/ src/theory/uf/symmetry_breaker.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/symmetry_breaker.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/theory_uf.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/theory_uf.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/theory_uf_model.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/theory_uf_model.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/theory_uf_rewriter.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/theory_uf_strong_solver.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/theory_uf_strong_solver.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/theory_uf_type_rules.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/valuation.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/valuation.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/abstract_value.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/uti l/abstract_value.h\ /wrkdirs/usr/ports/math/! cvc4/work! /CVC4-1.7/src/util/bin_heap.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/bitvector.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/bitvector.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/bool.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/cardinality.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/cardinality.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/channel.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/debug.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/dense_map.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/divisible.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/divisible.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/floatingpoint.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/gmp_util.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/hash.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/index.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/index.h \ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/integer_cln_imp.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/integer_cln_imp.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/integer_gmp_imp.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/integer_gmp_imp.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/maybe.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/ostream_util.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/ostream_util.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/proof.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/random.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/random.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/rational_cln_imp.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/rational_cln_imp.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/rational_gmp_imp.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/rational_gmp_imp.h\ /wrkdirs/usr/ports/math/cvc4/ work/CVC4-1.7/src/util/regexp.cpp\ /wrkdirs/! usr/ports! /math/cvc4/work/CVC4-1.7/src/util/regexp.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/resource_manager.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/resource_manager.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/result.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/result.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/safe_print.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/safe_print.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/sampler.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/sampler.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/sexpr.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/sexpr.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/smt2_quote_string.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/smt2_quote_string.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/statistics.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/statistics.h\ /wrkdirs/usr/ ports/math/cvc4/work/CVC4-1.7/src/util/statistics_registry.cpp\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/statistics_registry.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/tuple.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/unsafe_interrupt_exception.h\ /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/util/utility.h [ 1% 6/465] cd /wrkdirs/usr/ports/math/cvc4/work/.build/src/base && /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/gentags.sh Debug [ 1% 7/465] cd /wrkdirs/usr/ports/math/cvc4/work/.build/src/base && /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/genheader.sh /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base Debug [ 1% 8/465] cd /wrkdirs/usr/ports/math/cvc4/work/.build/src/base && /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/gentags.sh Trace [ 1% 9/465] cd /wrkdirs/usr/ports/math/cvc4/work/.build/src/base && /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base/genheader.sh /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/base Trace [ 1% 10/465] cd /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr && /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/mkexpr /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/expr_template.h /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/booleans/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/fp/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sep/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/kinds /wr kdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/kinds > /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr/expr.h FAILED: src/expr/expr.h /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr/expr.h cd /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr && /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/mkexpr /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/expr_template.h /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/booleans/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/fp/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sep/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/kinds /wrkdirs/usr/port s/math/cvc4/work/CVC4-1.7/src/theory/idl/kinds > /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr/expr.h /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/expr_template.h:0: error: undefined replacement ${getConst_instantiations} [ 2% 10/465] cd /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr && /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/mkkind /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/kind_template.cpp /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/booleans/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/bv/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/fp/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sep/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sets/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/kinds / wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/kinds > /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr/kind.cpp ninja: build stopped: subcommand failed. ===> Compilation failed unexpectedly. Try to set MAKE_JOBS_UNSAFE=yes and rebuild before reporting the failure to the maintainer. *** Error code 1 Stop. make: stopped in /usr/ports/math/cvc4