[package - 131amd64-quarterly][math/cvc4] Failed for cvc4-1.7_6 in build

Go to: [ bottom of page ] [ top of archives ] [ this month ]
From: <pkg-fallout_at_FreeBSD.org>
Date: Tue, 29 Nov 2022 01:13:08 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/beefy14/data/131amd64-quarterly/3b2b7d4f6a81/logs/cvc4-1.7_6.log
Build URL:      https://pkg-status.freebsd.org/beefy14/build.html?mastername=131amd64-quarterly&build=3b2b7d4f6a81
Log:

=>> Building math/cvc4
build started at Tue Nov 29 01:12:18 UTC 2022
port directory: /usr/ports/math/cvc4
package name: cvc4-1.7_6
building for: FreeBSD 131amd64-quarterly-job-10 13.1-RELEASE-p4 FreeBSD 13.1-RELEASE-p4 amd64
maintained by: ports@FreeBSD.org
Makefile ident: 
Poudriere version: 3.2.8-23-ga7f8d188
Host OSVERSION: 1400073
Jail OSVERSION: 1301000
Job Id: 10

---Begin Environment---
SHELL=/bin/csh
OSVERSION=1301000
UNAME_v=FreeBSD 13.1-RELEASE-p4
UNAME_r=13.1-RELEASE-p4
BLOCKSIZE=K
MAIL=/var/mail/root
MM_CHARSET=UTF-8
LANG=C.UTF-8
STATUS=1
HOME=/root
PATH=/sbin:/bin:/usr/sbin:/usr/bin:/usr/local/sbin:/usr/local/bin:/root/bin
LOCALBASE=/usr/local
USER=root
LIBEXECPREFIX=/usr/local/libexec/poudriere
POUDRIERE_VERSION=3.2.8-23-ga7f8d188
MASTERMNT=/usr/local/poudriere/data/.m/131amd64-quarterly/ref
POUDRIERE_BUILD_TYPE=bulk
PACKAGE_BUILDING=yes
SAVED_TERM=
PWD=/usr/local/poudriere/data/.m/131amd64-quarterly/ref/.p/pool
P_PORTS_FEATURES=FLAVORS SELECTED_OPTIONS
MASTERNAME=131amd64-quarterly
SCRIPTPREFIX=/usr/local/share/poudriere
OLDPWD=/usr/local/poudriere/data/.m/131amd64-quarterly/ref/.p
SCRIPTPATH=/usr/local/share/poudriere/bulk.sh
POUDRIEREPATH=/usr/local/bin/poudriere
---End Environment---

---Begin Poudriere Port Flags/Env---
PORT_FLAGS=
PKGENV=
FLAVOR=
DEPENDS_ARGS=
MAKE_ARGS=
---End Poudriere Port Flags/Env---

---Begin OPTIONS List---
===> The following configuration options are available for cvc4-1.7_6:
     CRYPTOMINISAT=on: Use CryptoMiniSat as the SAT solver
     JAVA=on: Java platform support
     PYTHON=on: Python bindings or support
     READLINE=on: Command line editing via libreadline
====> Options available for the radio NUMLIB: you can only select none or one of them
     GMP=on: Use GMP numeric library
     CLN=off: Use CLN numeric library (disables portfolio mode)
===> Use 'make config' to modify these settings
---End OPTIONS List---

--MAINTAINER--
ports@FreeBSD.org
--End MAINTAINER--

--CONFIGURE_ARGS--

--End CONFIGURE_ARGS--

--CONFIGURE_ENV--
PKG_CONFIG=pkgconf PYTHON="/usr/local/bin/python3.9" XDG_DATA_HOME=/wrkdirs/usr/ports/math/cvc4/work  XDG_CONFIG_HOME=/wrkdirs/usr/ports/math/cvc4/work  XDG_CACHE_HOME=/wrkdirs/usr/ports/math/cvc4/work/.cache  HOME=/wrkdirs/usr/ports/math/cvc4/work TMPDIR="/tmp" PATH=/wrkdirs/usr/ports/math/cvc4/work/.bin:/sbin:/bin:/usr/sbin:/usr/bin:/usr/local/sbin:/usr/local/bin:/root/bin PKG_CONFIG_LIBDIR=/wrkdirs/usr/ports/math/cvc4/work/.pkgconfig:/usr/local/libdata/pkgconfig:/usr/local/share/pkgconfig:/usr/libdata/pkgconfig SHELL=/bin/sh CONFIG_SHELL=/bin/sh
--End CONFIGURE_ENV--

--MAKE_ENV--
NINJA_STATUS="[%p %s/%t] " XDG_DATA_HOME=/wrkdirs/usr/ports/math/cvc4/work  XDG_CONFIG_HOME=/wrkdirs/usr/ports/math/cvc4/work  XDG_CACHE_HOME=/wrkdirs/usr/ports/math/cvc4/work/.cache  HOME=/wrkdirs/usr/ports/math/cvc4/work TMPDIR="/tmp" PATH=/wrkdirs/usr/ports/math/cvc4/work/.bin:/sbin:/bin:/usr/sbin:/usr/bin:/usr/local/sbin:/usr/local/bin:/root/bin PKG_CONFIG_LIBDIR=/wrkdirs/usr/ports/math/cvc4/work/.pkgconfig:/usr/local/libdata/pkgconfig:/usr/local/share/pkgconfig:/usr/libdata/pkgconfig NO_PIE=yes MK_DEBUG_FILES=no MK_KERNEL_SYMBOLS=no SHELL=/bin/sh NO_LINT=YES DESTDIR=/wrkdirs/usr/ports/math/cvc4/work/stage PREFIX=/usr/local  LOCALBASE=/usr/local  CC="cc" CFLAGS="-O2 -pipe  -fstack-protector-strong -fno-strict-aliasing "  CPP="cpp" CPPFLAGS="-I/usr/local/include"  LDFLAGS=" -L/usr/local/lib -fstack-protector-strong " LIBS=""  CXX="c++" CXXFLAGS="-O2 -pipe -fstack-protector-strong -fno-strict-aliasing  "  MANPREFIX="/usr/local" BSD_INSTALL_PROGRAM="install  -s -m 555"  BSD_INSTALL_
 LIB="install  -s -m 0644"  BSD_INSTALL_SCRIPT="install  -m 555"  BSD_INSTALL_DATA="install  -m 0644"  BSD_INSTALL_MAN="install  -m 444"
--End MAKE_ENV--

--PLIST_SUB--
CLN="@comment " NO_CLN="" CRYPTOMINISAT="" NO_CRYPTOMINISAT="@comment " GMP="" NO_GMP="@comment " JAVA="" NO_JAVA="@comment " PYTHON="" NO_PYTHON="@comment " READLINE="" NO_READLINE="@comment " JAVASHAREDIR="share/java"  JAVAJARDIR="share/java/classes" CMAKE_BUILD_TYPE="production" PYTHON_INCLUDEDIR=include/python3.9  PYTHON_LIBDIR=lib/python3.9  PYTHON_PLATFORM=freebsd13  PYTHON_SITELIBDIR=lib/python3.9/site-packages  PYTHON_SUFFIX=39  PYTHON_EXT_SUFFIX=.cpython-39  PYTHON_VER=3.9  PYTHON_VERSION=python3.9 PYTHON2="@comment " PYTHON3="" OSREL=13.1 PREFIX=%D LOCALBASE=/usr/local  RESETPREFIX=/usr/local LIB32DIR=lib DOCSDIR="share/doc/cvc4"  EXAMPLESDIR="share/examples/cvc4"  DATADIR="share/cvc4"  WWWDIR="www/cvc4"  ETCDIR="etc/cvc4"
--End PLIST_SUB--

--SUB_LIST--
CLN="@comment " NO_CLN="" CRYPTOMINISAT="" NO_CRYPTOMINISAT="@comment " GMP="" NO_GMP="@comment " JAVA="" NO_JAVA="@comment " PYTHON="" NO_PYTHON="@comment " READLINE="" NO_READLINE="@comment " JAVASHAREDIR="/usr/local/share/java"  JAVAJARDIR="/usr/local/share/java/classes"  JAVALIBDIR="/usr/local/share/java/classes" PREFIX=/usr/local LOCALBASE=/usr/local  DATADIR=/usr/local/share/cvc4 DOCSDIR=/usr/local/share/doc/cvc4 EXAMPLESDIR=/usr/local/share/examples/cvc4  WWWDIR=/usr/local/www/cvc4 ETCDIR=/usr/local/etc/cvc4
--End SUB_LIST--

---Begin make.conf---
USE_PACKAGE_DEPENDS=yes
BATCH=yes
WRKDIRPREFIX=/wrkdirs
PORTSDIR=/usr/ports
PACKAGES=/packages
DISTDIR=/distfiles
PACKAGE_BUILDING=yes
PACKAGE_BUILDING_FLAVORS=yes
#### /usr/local/etc/poudriere.d/make.conf ####
# XXX: We really need this but cannot use it while 'make checksum' does not
# try the next mirror on checksum failure.  It currently retries the same
# failed mirror and then fails rather then trying another.  It *does*
# try the next if the size is mismatched though.
#MASTER_SITE_FREEBSD=yes
# Build ALLOW_MAKE_JOBS_PACKAGES with 2 jobs
MAKE_JOBS_NUMBER=2
#### /usr/ports/Mk/Scripts/ports_env.sh ####
_CCVERSION_921dbbb2=FreeBSD clang version 13.0.0 (git@github.com:llvm/llvm-project.git llvmorg-13.0.0-0-gd7b669b3a303) Target: x86_64-unknown-freebsd13.1 Thread model: posix InstalledDir: /usr/bin
_ALTCCVERSION_921dbbb2=none
_CXXINTERNAL_acaad9ca=FreeBSD clang version 13.0.0 (git@github.com:llvm/llvm-project.git llvmorg-13.0.0-0-gd7b669b3a303) Target: x86_64-unknown-freebsd13.1 Thread model: posix InstalledDir: /usr/bin "/usr/bin/ld" "--eh-frame-hdr" "-dynamic-linker" "/libexec/ld-elf.so.1" "--hash-style=both" "--enable-new-dtags" "-o" "a.out" "/usr/lib/crt1.o" "/usr/lib/crti.o" "/usr/lib/crtbegin.o" "-L/usr/lib" "/dev/null" "-lc++" "-lm" "-lgcc" "--as-needed" "-lgcc_s" "--no-as-needed" "-lc" "-lgcc" "--as-needed" "-lgcc_s" "--no-as-needed" "/usr/lib/crtend.o" "/usr/lib/crtn.o"
CC_OUTPUT_921dbbb2_58173849=yes
CC_OUTPUT_921dbbb2_9bdba57c=yes
CC_OUTPUT_921dbbb2_6a4fe7f5=yes
CC_OUTPUT_921dbbb2_6bcac02b=yes
CC_OUTPUT_921dbbb2_67d20829=yes
CC_OUTPUT_921dbbb2_bfa62e83=yes
CC_OUTPUT_921dbbb2_f0b4d593=yes
CC_OUTPUT_921dbbb2_308abb44=yes
CC_OUTPUT_921dbbb2_f00456e5=yes
CC_OUTPUT_921dbbb2_65ad290d=yes
CC_OUTPUT_921dbbb2_f2776b26=yes
CC_OUTPUT_921dbbb2_53255a77=yes
CC_OUTPUT_921dbbb2_911cfe02=yes
CC_OUTPUT_921dbbb2_b2657cc3=yes
CC_OUTPUT_921dbbb2_380987f7=yes
CC_OUTPUT_921dbbb2_160933ec=yes
CC_OUTPUT_921dbbb2_fb62803b=yes
CC_OUTPUT_921dbbb2_af59ad06=yes
CC_OUTPUT_921dbbb2_a15f3fcf=yes
_OBJC_CCVERSION_921dbbb2=FreeBSD clang version 13.0.0 (git@github.com:llvm/llvm-project.git llvmorg-13.0.0-0-gd7b669b3a303) Target: x86_64-unknown-freebsd13.1 Thread model: posix InstalledDir: /usr/bin
_OBJC_ALTCCVERSION_921dbbb2=none
ARCH=amd64
OPSYS=FreeBSD
_OSRELEASE=13.1-RELEASE-p4
OSREL=13.1
OSVERSION=1301000
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
[131amd64-quarterly-job-10] Installing pkg-1.18.4...
[131amd64-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       >============================
<snip>
-- Looking for unistd.h - found
-- Looking for C++ include ext/stdio_filebuf.h
-- Looking for C++ include ext/stdio_filebuf.h - not found
-- Looking for clock_gettime
-- Looking for clock_gettime - found
-- Looking for ffs
-- Looking for ffs - found
-- Looking for optreset
-- Looking for optreset - found
-- Looking for sigaltstack
-- Looking for sigaltstack - found
-- Looking for strerror_r
-- Looking for strerror_r - found
-- Looking for strtok_r
-- Looking for strtok_r - found
-- Performing Test STRERROR_R_CHAR_P
-- Performing Test STRERROR_R_CHAR_P - Failed
-- Found Boost: /usr/local/include (found suitable version "1.80.0", minimum required is "1.50.0")  
-- Found Java: /usr/local/bin/java (found version "1.8.0.342") 
-- Could NOT find Git (missing: GIT_EXECUTABLE) 
-- Looking for antlr3FileStreamNew
-- Looking for antlr3FileStreamNew - found
-- Found ANTLR: /wrkdirs/usr/ports/math/cvc4/work/antlr3  
-- Found ANTLR libs: /usr/local/lib/libantlr3c.so
-- Found Java: /usr/local/bin/java (found version "1.8.0.342") found components: Runtime 
-- Found SWIG: /usr/local/bin/swig (found suitable version "4.0.2", minimum required is "3.0.0")  
-- Found Java: /usr/local/bin/java (found version "1.8.0.342") 
-- Found JNI: /usr/local/openjdk8/include  found components: AWT JVM 
CMake Warning (dev) at /usr/local/share/cmake/Modules/UseSWIG.cmake:775 (message):
  Policy CMP0078 is not set: UseSWIG generates standard target names.  Run
  "cmake --help-policy CMP0078" for policy details.  Use the cmake_policy
  command to set the policy and suppress this warning.

Call Stack (most recent call first):
  src/bindings/java/CMakeLists.txt:14 (swig_add_library)
This warning is for project developers.  Use -Wno-dev to suppress it.

CMake Warning (dev) at /usr/local/share/cmake/Modules/UseSWIG.cmake:617 (message):
  Policy CMP0086 is not set: UseSWIG honors SWIG_MODULE_NAME via -module
  flag.  Run "cmake --help-policy CMP0086" for policy details.  Use the
  cmake_policy command to set the policy and suppress this warning.

Call Stack (most recent call first):
  /usr/local/share/cmake/Modules/UseSWIG.cmake:888 (SWIG_ADD_SOURCE_TO_MODULE)
  src/bindings/java/CMakeLists.txt:14 (swig_add_library)
This warning is for project developers.  Use -Wno-dev to suppress it.

-- Found PythonLibs: /usr/local/lib/libpython3.9.so (found suitable version "3.9.15", minimum required is "3.9") 
CMake Warning (dev) at /usr/local/share/cmake/Modules/UseSWIG.cmake:775 (message):
  Policy CMP0078 is not set: UseSWIG generates standard target names.  Run
  "cmake --help-policy CMP0078" for policy details.  Use the cmake_policy
  command to set the policy and suppress this warning.

Call Stack (most recent call first):
  src/bindings/python/CMakeLists.txt:23 (swig_add_library)
This warning is for project developers.  Use -Wno-dev to suppress it.

CMake Warning (dev) at /usr/local/share/cmake/Modules/UseSWIG.cmake:617 (message):
  Policy CMP0086 is not set: UseSWIG honors SWIG_MODULE_NAME via -module
  flag.  Run "cmake --help-policy CMP0086" for policy details.  Use the
  cmake_policy command to set the policy and suppress this warning.

Call Stack (most recent call first):
  /usr/local/share/cmake/Modules/UseSWIG.cmake:888 (SWIG_ADD_SOURCE_TO_MODULE)
  src/bindings/python/CMakeLists.txt:23 (swig_add_library)
This warning is for project developers.  Use -Wno-dev to suppress it.

CVC4 1.7

Build profile        : production

GPL                  : on
Best configuration   : off
Optimized            : on
Optimization level   : off

Assertions           : off
Debug symbols        : off
Debug context mem mgr: off

Dumping              : off
Muzzle               : off
Proofs               : on
Replay               : off
Statistics           : on
Tracing              : off

Asan                 : off
Coverage (gcov)      : off
Profiling (gprof)    : off
Unit tests           : off
Valgrind             : off

Shared libs          : on
Static binary        : off
Java bindings        : off
Python bindings      : off
Python2              : off
Python3              : off

Portfolio            : off

ABC                  : off
CaDiCaL              : off
CryptoMiniSat        : off
drat2er              : off
GLPK                 : off
LFSC                 : off
MP library           : gmp
Readline             : off
SymFPU               : off


CPPLAGS (-D...)      : NDEBUG CVC4_PORTFOLIO CVC4_PROOF CVC4_STATISTICS_ON CVC4_USE_CRYPTOMINISAT
CXXFLAGS             : -O2 -pipe -fstack-protector-strong -fno-strict-aliasing -O3 -Wall -Wno-deprecated -Wsuggest-override -Wnon-virtual-dtor -pthread -pthread
CFLAGS               : -O2 -pipe  -fstack-protector-strong -fno-strict-aliasing -O3 -Wall -fexceptions -Wno-deprecated -pthread -pthread

Install prefix       : /usr/local

CVC4 license         : GPLv3 (due to optional libraries; see below)

Please note that CVC4 will be built against the following GPLed libraries:
 readline
As these libraries are covered under the GPLv3, so is this build of CVC4.
CVC4 is also available to you under the terms of the (modified) BSD license.
If you prefer to license CVC4 under those terms, please configure CVC4 to
disable all optional GPLed library dependencies (-DENABLE_BSD_ONLY=ON).

Now just type make, followed by make check or make install.

-- Configuring done
-- Generating done
CMake Warning (dev):
  Policy CMP0058 is not set: Ninja requires custom command byproducts to be
  explicit.  Run "cmake --help-policy CMP0058" for policy details.  Use the
  cmake_policy command to set the policy and suppress this warning.

  This project specifies custom command DEPENDS on files in the build tree
  that are not specified as the OUTPUT or BYPRODUCTS of any
  add_custom_command or add_custom_target:

   src/base/Debug_tags.tmp
   src/base/Trace_tags.tmp
   src/bindings/java/ArrayStoreAll.java
   src/bindings/java/ArrayStoreAllHashFunction.java
   src/bindings/java/ArrayType.java
   src/bindings/java/AscriptionType.java
   src/bindings/java/AscriptionTypeHashFunction.java
   src/bindings/java/AssertCommand.java
   src/bindings/java/BenchmarkStatus.java
   src/bindings/java/BitVector.java

  For compatibility with versions of CMake that did not have the BYPRODUCTS
  option, CMake is generating phony rules for such files to convince 'ninja'
  to build.

  Project authors should add the missing BYPRODUCTS or OUTPUT options to the
  custom commands that produce these files.
This warning is for project developers.  Use -Wno-dev to suppress it.

CMake Warning:
  Manually-specified variables were not used by the project:

    CMAKE_COLOR_MAKEFILE
    CMAKE_CXX_FLAGS_DEBUG
    CMAKE_CXX_FLAGS_RELEASE
    CMAKE_C_FLAGS_DEBUG
    CMAKE_C_FLAGS_RELEASE
    CMAKE_VERBOSE_MAKEFILE


-- Build files have been written to: /wrkdirs/usr/ports/math/cvc4/work/.build
===========================================================================
=======================<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/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
[  2% 11/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% 11/465] cd /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr && /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/mkmetakind /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/metakind_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/k
 inds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/kinds > /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr/metakind.h
FAILED: src/expr/metakind.h /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr/metakind.h 
cd /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr && /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/mkmetakind /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/metakind_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/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/kinds > /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr/metakind.h
/wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/metakind_template.h:0: error: undefined replacement ${metakind_getConst_decls}
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