[package - 123amd64-quarterly][math/cvc4] Failed for cvc4-1.7_6 in build
- Go to: [ bottom of page ] [ top of archives ] [ this month ]
Date: Sat, 24 Dec 2022 01:08:04 UTC
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: https://pkg-status.freebsd.org/beefy2/data/123amd64-quarterly/0597389d2088/logs/cvc4-1.7_6.log
Build URL: https://pkg-status.freebsd.org/beefy2/build.html?mastername=123amd64-quarterly&build=0597389d2088
Log:
=>> Building math/cvc4
build started at Sat Dec 24 01:07:33 UTC 2022
port directory: /usr/ports/math/cvc4
package name: cvc4-1.7_6
building for: FreeBSD 123amd64-quarterly-job-10 12.3-RELEASE-p10 FreeBSD 12.3-RELEASE-p10 amd64
maintained by: ports@FreeBSD.org
Makefile ident:
Poudriere version: 3.2.8-23-ga7f8d188
Host OSVERSION: 1400073
Jail OSVERSION: 1203000
Job Id: 10
---Begin Environment---
SHELL=/bin/csh
OSVERSION=1203000
UNAME_v=FreeBSD 12.3-RELEASE-p10
UNAME_r=12.3-RELEASE-p10
BLOCKSIZE=K
MAIL=/var/mail/root
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-23-ga7f8d188
MASTERMNT=/usr/local/poudriere/data/.m/123amd64-quarterly/ref
POUDRIERE_BUILD_TYPE=bulk
PACKAGE_BUILDING=yes
SAVED_TERM=
PWD=/usr/local/poudriere/data/.m/123amd64-quarterly/ref/.p/pool
P_PORTS_FEATURES=FLAVORS SELECTED_OPTIONS
MASTERNAME=123amd64-quarterly
SCRIPTPREFIX=/usr/local/share/poudriere
OLDPWD=/usr/local/poudriere/data/.m/123amd64-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=freebsd12 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=12.3 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
#### /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 10.0.1 (git@github.com:llvm/llvm-project.git llvmorg-10.0.1-0-gef32c611aa2) Target: x86_64-unknown-freebsd12.3 Thread model: posix InstalledDir: /usr/bin
_ALTCCVERSION_921dbbb2=none
_CXXINTERNAL_acaad9ca=FreeBSD clang version 10.0.1 (git@github.com:llvm/llvm-project.git llvmorg-10.0.1-0-gef32c611aa2) Target: x86_64-unknown-freebsd12.3 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" "-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=error: invalid value 'c++2b' in '-std=c++2b' note: use 'c++98' or 'c++03' for 'ISO C++ 1998 with amendments' standard note: use 'gnu++98' or 'gnu++03' for 'ISO C++ 1998 with amendments and GNU extensions' standard note: use 'c++11' for 'ISO C++ 2011 with amendments' standard note: use 'gnu++11' for 'ISO C++ 2011 with amendments and GNU extensions' standard note: use 'c++14' for 'ISO C++ 2014 with amendments' standard note: use 'gnu++14' for 'ISO C++ 2014 with amendments and GNU extensions' standard note: use 'c++17' for 'ISO C++ 2017 with amendments' standard note: use 'gnu++17' for 'ISO C++ 2017 with amendments and GNU extensions' standard note: use 'c++20' for 'ISO C++ 2020 DIS' standard note: use 'gnu++20' for 'ISO C++ 2020 DIS with GNU extensions' standard
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=error: invalid value 'gnu++2b' in '-std=gnu++2b' note: use 'c++98' or 'c++03' for 'ISO C++ 1998 with amendments' standard note: use 'gnu++98' or 'gnu++03' for 'ISO C++ 1998 with amendments and GNU extensions' standard note: use 'c++11' for 'ISO C++ 2011 with amendments' standard note: use 'gnu++11' for 'ISO C++ 2011 with amendments and GNU extensions' standard note: use 'c++14' for 'ISO C++ 2014 with amendments' standard note: use 'gnu++14' for 'ISO C++ 2014 with amendments and GNU extensions' standard note: use 'c++17' for 'ISO C++ 2017 with amendments' standard note: use 'gnu++17' for 'ISO C++ 2017 with amendments and GNU extensions' standard note: use 'c++20' for 'ISO C++ 2020 DIS' standard note: use 'gnu++20' for 'ISO C++ 2020 DIS with GNU extensions' standard
_OBJC_CCVERSION_921dbbb2=FreeBSD clang version 10.0.1 (git@github.com:llvm/llvm-project.git llvmorg-10.0.1-0-gef32c611aa2) Target: x86_64-unknown-freebsd12.3 Thread model: posix InstalledDir: /usr/bin
_OBJC_ALTCCVERSION_921dbbb2=none
ARCH=amd64
OPSYS=FreeBSD
_OSRELEASE=12.3-RELEASE-p10
OSREL=12.3
OSVERSION=1203000
PYTHONBASE=/usr/local
HAVE_COMPAT_IA32_KERN=YES
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) 33554432
stack size (kbytes, -s) 524288
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--
=======================<phase: check-sanity >============================
===> 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
===========================================================================
=======================<phase: pkg-depends >============================
===> cvc4-1.7_6 depends on file: /usr/local/sbin/pkg - not found
===> Installing existing package /packages/All/pkg-1.18.4.pkg
[123amd64-quarterly-job-10] Installing pkg-1.18.4...
[123amd64-quarterly-job-10] 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
===========================================================================
=======================<phase: fetch-depends >============================
===========================================================================
=======================<phase: fetch >============================
===> 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
===> Fetching all distfiles required by cvc4-1.7_6 for building
===========================================================================
=======================<phase: checksum >============================
===> NOTICE:
<snip>
-- Performing Test CVC4_NEED_INT64_T_OVERLOADS - Failed
-- 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.16", 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 -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
===========================================================================
=======================<phase: 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