Removing unused build options and deprecated proof compile flag (#6195)

33 files changed, 29 insertions, 262 deletions

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index e1ea39011..ad6004251 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -23,7 +23,7 @@ jobs:
 
         include:
           - name: production
-            config: production --all-bindings --lfsc --editline --poly --symfpu
+            config: production --all-bindings --editline --poly --symfpu
             cache-key: production
             python-bindings: true
             check-examples: true
@@ -40,7 +40,7 @@ jobs:
             run_regression_args: --no-check-unsat-cores --no-check-proofs
 
           - name: production-dbg
-            config: production --assertions --tracing --unit-testing --symfpu --lfsc --editline
+            config: production --assertions --tracing --unit-testing --symfpu --editline
             cache-key: dbg
             os: ubuntu-latest
             exclude_regress: 3-4
@@ -198,4 +198,3 @@ jobs:
         make -j2
         ctest -j2 --output-on-failure
       working-directory: examples
-
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 1bbe6d288..7d0c98be2 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -70,9 +70,6 @@ endif()
 if(CRYPTOMINISAT_DIR)
   list(APPEND CMAKE_PREFIX_PATH "${CRYPTOMINISAT_DIR}")
 endif()
-if(DRAT2ER_DIR)
-  list(APPEND CMAKE_PREFIX_PATH "${DRAT2ER_DIR}")
-endif()
 if(GLPK_DIR)
   list(APPEND CMAKE_PREFIX_PATH "${GLPK_DIR}")
 endif()
@@ -82,9 +79,6 @@ endif()
 if(KISSAT_DIR)
   list(APPEND CMAKE_PREFIX_PATH "${KISSAT_DIR}")
 endif()
-if(LFSC_DIR)
-  list(APPEND CMAKE_PREFIX_PATH "${LFSC_DIR}")
-endif()
 if(POLY_DIR)
   list(APPEND CMAKE_PREFIX_PATH "${POLY_DIR}")
 endif()
@@ -119,7 +113,6 @@ cvc4_option(ENABLE_COMP_INC_TRACK
 cvc4_option(ENABLE_DEBUG_SYMBOLS  "Enable debug symbols")
 cvc4_option(ENABLE_DUMPING        "Enable dumping")
 cvc4_option(ENABLE_MUZZLE         "Suppress ALL non-result output")
-cvc4_option(ENABLE_PROOFS         "Enable proof support")
 cvc4_option(ENABLE_STATISTICS     "Enable statistics")
 cvc4_option(ENABLE_TRACING        "Enable tracing")
 cvc4_option(ENABLE_UNIT_TESTING   "Enable unit testing")
@@ -148,8 +141,6 @@ cvc4_option(USE_KISSAT        "Use Kissat SAT solver")
 cvc4_option(USE_EDITLINE      "Use Editline for better interactive support")
 # >> 2-valued: ON OFF
 #    > for options where we don't need to detect if set by user (default: OFF)
-option(USE_DRAT2ER            "Include drat2er for making eager BV proofs")
-option(USE_LFSC               "Use LFSC proof checker")
 option(USE_POLY               "Use LibPoly for polynomial arithmetic")
 option(USE_SYMFPU             "Use SymFPU for floating point support")
 option(USE_PYTHON2            "Force Python 2 (deprecated)")
@@ -163,11 +154,9 @@ set(ABC_DIR           "" CACHE STRING "Set ABC install directory")
 set(ANTLR_DIR         "" CACHE STRING "Set ANTLR3 install directory")
 set(CADICAL_DIR       "" CACHE STRING "Set CaDiCaL install directory")
 set(CRYPTOMINISAT_DIR "" CACHE STRING "Set CryptoMiniSat install directory")
-set(DRAT2ER_DIR       "" CACHE STRING "Set drat2er install directory")
 set(GLPK_DIR          "" CACHE STRING "Set GLPK install directory")
 set(GMP_DIR           "" CACHE STRING "Set GMP install directory")
 set(KISSAT_DIR        "" CACHE STRING "Set Kissat install directory")
-set(LFSC_DIR          "" CACHE STRING "Set LFSC install directory")
 set(POLY_DIR          "" CACHE STRING "Set LibPoly install directory")
 set(SYMFPU_DIR        "" CACHE STRING "Set SymFPU install directory")
 
@@ -429,10 +418,6 @@ if(ENABLE_PROFILING)
   add_check_c_cxx_flag("-pg")
 endif()
 
-if(ENABLE_PROOFS)
-  add_definitions(-DCVC4_PROOF)
-endif()
-
 if(ENABLE_TRACING)
   add_definitions(-DCVC4_TRACING)
 endif()
@@ -477,11 +462,6 @@ if(USE_CRYPTOMINISAT)
   add_definitions(-DCVC4_USE_CRYPTOMINISAT)
 endif()
 
-if(USE_DRAT2ER)
-  find_package(Drat2Er REQUIRED)
-  add_definitions(-DCVC4_USE_DRAT2ER)
-endif()
-
 if(USE_GLPK)
   set(GPL_LIBS "${GPL_LIBS} glpk")
   find_package(GLPK REQUIRED)
@@ -493,11 +473,6 @@ if(USE_KISSAT)
   add_definitions(-DCVC4_USE_KISSAT)
 endif()
 
-if(USE_LFSC)
-  find_package(LFSC REQUIRED)
-  add_definitions(-DCVC4_USE_LFSC)
-endif()
-
 if(USE_POLY)
   find_package(Poly REQUIRED)
   add_definitions(-DCVC4_USE_POLY)
@@ -550,11 +525,6 @@ include_directories(${CMAKE_CURRENT_BINARY_DIR})
 #-----------------------------------------------------------------------------#
 # Add subdirectories
 
-# signatures needs to come before src since it adds source files to libcvc4.
-if(ENABLE_PROOFS)
-  add_subdirectory(proofs/signatures)
-endif()
-
 add_subdirectory(doc)
 add_subdirectory(src)
 add_subdirectory(test)
@@ -580,7 +550,7 @@ include(CMakePackageConfigHelpers)
 # libraries from deps/install/lib, we need to be cautious. Changing these
 # shared libraries from deps/install/lib most probably breaks the binary.
 # We only allow such an installation for custom installation prefixes
-# (in the assumption that only reasonably experienced users use this and 
+# (in the assumption that only reasonably experienced users use this and
 # also that custom installation prefixes are not used for longer periods of
 # time anyway). Also, we print a big warning with further instructions.
 if(NOT ENABLE_STATIC_BINARY)
@@ -695,10 +665,8 @@ message("")
 print_config("ABC                       :" USE_ABC)
 print_config("CaDiCaL                   :" USE_CADICAL)
 print_config("CryptoMiniSat             :" USE_CRYPTOMINISAT)
-print_config("drat2er                   :" USE_DRAT2ER)
 print_config("GLPK                      :" USE_GLPK)
 print_config("Kissat                    :" USE_KISSAT)
-print_config("LFSC                      :" USE_LFSC)
 print_config("LibPoly                   :" USE_POLY)
 message("")
 print_config("Build libcvc4 only        :" BUILD_LIB_ONLY)
@@ -723,9 +691,6 @@ endif()
 if(CRYPTOMINISAT_DIR)
   message("CRYPTOMINISAT dir         : ${CRYPTOMINISAT_DIR}")
 endif()
-if(DRAT2ER_DIR)
-  message("DRAT2ER dir               : ${DRAT2ER_DIR}")
-endif()
 if(GLPK_DIR)
   message("GLPK dir                  : ${GLPK_DIR}")
 endif()
@@ -735,9 +700,6 @@ endif()
 if(KISSAT_DIR)
   message("KISSAT dir                : ${KISSAT_DIR}")
 endif()
-if(LFSC_DIR)
-  message("LFSC dir                  : ${LFSC_DIR}")
-endif()
 if(POLY_DIR)
   message("LibPoly dir               : ${POLY_DIR}")
 endif()
diff --git a/COPYING b/COPYING
index d6f66b097..b181eb668 100644
--- a/COPYING
+++ b/COPYING
@@ -78,7 +78,6 @@ CVC4 optionally links against the following libraries:
   ABC                (https://bitbucket.org/alanmi/abc)
   CaDiCaL            (https://github.com/arminbiere/cadical)
   CryptoMiniSat      (https://github.com/msoos/cryptominisat)
-  LFSC checker       (https://github.com/CVC4/LFSC)
   LibPoly            (https://github.com/SRI-CSL/libpoly)
   libedit            (https://thrysoee.dk/editline)
 
@@ -108,4 +107,3 @@ CVC4 can be optionally configured to link against glpk-cut-log, a modified
 version of GLPK, the GNU Linear Programming Kit, available here:
 
   https://github.com/timothy-king/glpk-cut-log
-
diff --git a/INSTALL.md b/INSTALL.md
index 635118f1d..2d124b2af 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -41,7 +41,7 @@ can be found in `<build_dir>/lib`.
 
 ## Build dependencies
 
-The following tools and libraries are required to build and run CVC4.  
+The following tools and libraries are required to build and run CVC4.
 Versions given are minimum versions; more recent versions should be
 compatible.
 
@@ -95,7 +95,7 @@ want and should use.
 is an implementation of SMT-LIB/IEEE-754 floating-point operations in terms
 of bit-vector operations.
 It is required for supporting the theory of floating-point numbers and
-can be installed using the `contrib/get-symfpu` script.  
+can be installed using the `contrib/get-symfpu` script.
 Configure CVC4 with `configure.sh --symfpu` to build with this dependency.
 
 ### CaDiCaL (Optional SAT solver)
@@ -103,7 +103,7 @@ Configure CVC4 with `configure.sh --symfpu` to build with this dependency.
 [CaDiCaL](https://github.com/arminbiere/cadical)
 is a SAT solver that can be used for solving non-incremental bit-vector
 problems with eager bit-blasting. This dependency may improve performance.
-It can be installed using the `contrib/get-cadical script`.  
+It can be installed using the `contrib/get-cadical script`.
 Configure CVC4 with `configure.sh --cadical` to build with this dependency.
 
 ### CryptoMiniSat (Optional SAT solver)
@@ -111,7 +111,7 @@ Configure CVC4 with `configure.sh --cadical` to build with this dependency.
 [CryptoMinisat](https://github.com/msoos/cryptominisat)
 is a SAT solver that can be used for solving bit-vector problems with eager
 bit-blasting. This dependency may improve performance.
-It can be installed using the `contrib/get-cryptominisat` script.  
+It can be installed using the `contrib/get-cryptominisat` script.
 Configure CVC4 with `configure.sh --cryptominisat` to build with this
 dependency.
 
@@ -120,16 +120,10 @@ dependency.
 [Kissat](https://github.com/arminbiere/kissat)
 is a SAT solver that can be used for solving bit-vector problems with eager
 bit-blasting. This dependency may improve performance.
-It can be installed using the `contrib/get-kissat` script.  
+It can be installed using the `contrib/get-kissat` script.
 Configure CVC4 with `configure.sh --kissat` to build with this
 dependency.
 
-### LFSC (The LFSC Proof Checker)
-
-[LFSC](https://github.com/CVC4/LFSC) is required to check proofs internally
-with --check-proofs. It can be installed using the `contrib/get-lfsc` script.  
-Configure CVC4 with `configure.sh --lfsc` to build with this dependency.
-
 ### LibPoly (Optional polynomial library)
 
 [LibPoly](https://github.com/SRI-CSL/libpoly) is required for CAD-based nonlinear reasoning.
@@ -140,7 +134,7 @@ Configure CVC4 with `configure.sh --poly` to build with this dependency.
 
 [CLN](http://www.ginac.de/CLN)
 is an alternative multiprecision arithmetic package that may offer better
-performance and memory footprint than GMP.  
+performance and memory footprint than GMP.
 Configure CVC4 with `configure.sh --cln` to build with this dependency.
 
 Note that CLN is covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html).
@@ -158,7 +152,7 @@ implementation in CVC4. (This is not recommended for most users.)
 
 glpk-cut-log can be installed using the `contrib/get-glpk-cut-log` script.
 Note that the only installation option is manual installation via this script.
-CVC4 is no longer compatible with the main GLPK library.  
+CVC4 is no longer compatible with the main GLPK library.
 Configure CVC4 with `configure.sh --glpk` to build with this dependency.
 
 Note that GLPK and glpk-cut-log are covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html).
@@ -174,7 +168,7 @@ logic circuits. This dependency may improve performance of the eager
 bit-vector solver. When enabled, the bit-blasted formula is encoded into
 and-inverter-graphs (AIG) and ABC is used to simplify these AIGs.
 
-ABC can be installed using the `contrib/get-abc` script.  
+ABC can be installed using the `contrib/get-abc` script.
 Configure CVC4 with `configure.sh --abc` to build with this dependency.
 
 ### Editline library (Improved Interactive Experience)
@@ -192,7 +186,7 @@ provided with CVC4.
 ### Google Test Unit Testing Framework (Unit Tests)
 
 [Google Test](https://github.com/google/googletest) is required to optionally
-run CVC4's unit tests (included with the distribution). 
+run CVC4's unit tests (included with the distribution).
 See [Testing CVC4](#Testing-CVC4) below for more details.
 
 ## Language bindings
@@ -245,7 +239,7 @@ The system tests are not built by default.
 All system test binaries are built into `<build_dir>/bin/test/system`.
 
 We use prefix `api/` + `<api_test>` (for `<api_test>` in `test/api`)
-as test target name.  
+as test target name.
 
     make ouroborous                       # build test/api/ouroborous.cpp
     ctest -R ouroborous                   # run all tests that match '*ouroborous*'
@@ -268,7 +262,7 @@ assertions enabled.
 All unit test binaries are built into `<build_dir>/bin/test/unit`.
 
 We use prefix `unit/` + `<subdir>/` + `<unit_test>` (for `<unit_test>` in
-`test/unit/<subdir>`) as test target name.  
+`test/unit/<subdir>`) as test target name.
 
     make map_util_black                   # build test/unit/base/map_util_black.cpp
     ctest -R map_util_black               # run all tests that match '*map_util_black*'
@@ -281,7 +275,7 @@ We use prefix `unit/` + `<subdir>/` + `<unit_test>` (for `<unit_test>` in
 ### Testing Regression Tests
 
 We use prefix `regressN/` + `<subdir>/` + `<regress_test>` (for `<regress_test>`
-in level `N` in `test/regress/regressN/<subdir>`) as test target name.  
+in level `N` in `test/regress/regressN/<subdir>`) as test target name.
 
     ctest -L regress                      # run all regression tests
     ctest -L regress0                     # run all regression tests in level 0
@@ -295,23 +289,23 @@ in level `N` in `test/regress/regressN/<subdir>`) as test target name.
 
 All custom test targets build and run a preconfigured set of tests.
 
-- `make check [-jN] [ARGS=-jN]`  
+- `make check [-jN] [ARGS=-jN]`
   The default build-and-test target for CVC4, builds and runs all examples,
   all system and unit tests, and regression tests from levels 0 to 2.
 
-- `make systemtests [-jN] [ARGS=-jN]`  
+- `make systemtests [-jN] [ARGS=-jN]`
   Build and run all system tests.
 
-- `make units [-jN] [ARGS=-jN]`  
+- `make units [-jN] [ARGS=-jN]`
   Build and run all unit tests.
 
-- `make regress [-jN] [ARGS=-jN]`  
+- `make regress [-jN] [ARGS=-jN]`
   Build and run regression tests from levels 0 to 2.
 
-- `make runexamples [-jN] [ARGS=-jN]`  
+- `make runexamples [-jN] [ARGS=-jN]`
   Build and run all examples.
 
-- `make coverage [-jN] [ARGS=-jN]`  
+- `make coverage [-jN] [ARGS=-jN]`
   Build and run all tests (system and unit tests, regression tests level 0-4)
   with gcov to determine code coverage.
 
diff --git a/configure.sh b/configure.sh
index d57bcd5d5..43925a504 100755
--- a/configure.sh
+++ b/configure.sh
@@ -32,7 +32,6 @@ The following flags enable optional features (disable with --no-<option name>).
   --static                 build static libraries and binaries [default=no]
   --static-binary          statically link against system libraries
                            (must be disabled for static macOS builds) [default=yes]
-  --proofs                 support for proof generation
   --debug-symbols          include debug symbols
   --valgrind               Valgrind instrumentation
   --debug-context-mm       use the debug context memory manager
@@ -60,9 +59,7 @@ The following flags enable optional packages (disable with --no-<option name>).
   --abc                    use the ABC AIG library
   --cadical                use the CaDiCaL SAT solver
   --cryptominisat          use the CryptoMiniSat SAT solver
-  --drat2er                use drat2er (required for eager BV proofs)
   --kissat                 use the Kissat SAT solver
-  --lfsc                   use the LFSC proof checker
   --poly                   use the LibPoly library
   --symfpu                 use SymFPU for floating point solver
   --editline               support the editline library
@@ -72,11 +69,9 @@ Optional Path to Optional Packages:
   --antlr-dir=PATH         path to ANTLR C headers and libraries
   --cadical-dir=PATH       path to top level of CaDiCaL source tree
   --cryptominisat-dir=PATH path to top level of CryptoMiniSat source tree
-  --drat2er-dir=PATH       path to the top level of the drat2er installation
   --glpk-dir=PATH          path to top level of GLPK installation
   --gmp-dir=PATH           path to top level of GMP installation
   --kissat-dir=PATH        path to top level of Kissat source tree
-  --lfsc-dir=PATH          path to top level of LFSC source tree
   --poly-dir=PATH          path to top level of LibPoly source tree
   --symfpu-dir=PATH        path to top level of SymFPU source tree
 
@@ -123,17 +118,14 @@ coverage=default
 cryptominisat=default
 debug_context_mm=default
 debug_symbols=default
-drat2er=default
 dumping=default
 glpk=default
 gpl=default
 kissat=default
-lfsc=default
 poly=default
 muzzle=default
 ninja=default
 profiling=default
-proofs=default
 python2=default
 python_bindings=default
 java_bindings=default
@@ -155,11 +147,9 @@ abc_dir=default
 antlr_dir=default
 cadical_dir=default
 cryptominisat_dir=default
-drat2er_dir=default
 glpk_dir=default
 gmp_dir=default
 kissat_dir=default
-lfsc_dir=default
 poly_dir=default
 symfpu_dir=default
 
@@ -235,9 +225,6 @@ do
     --debug-context-mm) debug_context_mm=ON;;
     --no-debug-context-mm) debug_context_mm=OFF;;
 
-    --drat2er) drat2er=ON;;
-    --no-drat2er) drat2er=OFF;;
-
     --dumping) dumping=ON;;
     --no-dumping) dumping=OFF;;
 
@@ -256,18 +243,12 @@ do
     --glpk) glpk=ON;;
     --no-glpk) glpk=OFF;;
 
-    --lfsc) lfsc=ON;;
-    --no-lfsc) lfsc=OFF;;
-
     --poly) poly=ON;;
     --no-poly) poly=OFF;;
 
     --muzzle) muzzle=ON;;
     --no-muzzle) muzzle=OFF;;
 
-    --proofs) proofs=ON;;
-    --no-proofs) proofs=OFF;;
-
     --static) shared=OFF; static_binary=ON;;
     --no-static) shared=ON;;
 
@@ -320,9 +301,6 @@ do
     --cryptominisat-dir) die "missing argument to $1 (try -h)" ;;
     --cryptominisat-dir=*) cryptominisat_dir=${1##*=} ;;
 
-    --drat2er-dir) die "missing argument to $1 (try -h)" ;;
-    --drat2er-dir=*) drat2er_dir=${1##*=} ;;
-
     --glpk-dir) die "missing argument to $1 (try -h)" ;;
     --glpk-dir=*) glpk_dir=${1##*=} ;;
 
@@ -332,9 +310,6 @@ do
     --kissat-dir) die "missing argument to $1 (try -h)" ;;
     --kissat-dir=*) kissat_dir=${1##*=} ;;
 
-    --lfsc-dir) die "missing argument to $1 (try -h)" ;;
-    --lfsc-dir=*) lfsc_dir=${1##*=} ;;
-
     --poly-dir) die "missing argument to $1 (try -h)" ;;
     --poly-dir=*) poly_dir=${1##*=} ;;
 
@@ -411,8 +386,6 @@ cmake_opts=""
 [ $ninja != default ] && cmake_opts="$cmake_opts -G Ninja"
 [ $muzzle != default ] \
   && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle"
-[ $proofs != default ] \
-  && cmake_opts="$cmake_opts -DENABLE_PROOFS=$proofs"
 [ $shared != default ] \
   && cmake_opts="$cmake_opts -DENABLE_SHARED=$shared"
 [ $static_binary != default ] \
@@ -443,14 +416,10 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DUSE_CLN=$cln"
 [ $cryptominisat != default ] \
   && cmake_opts="$cmake_opts -DUSE_CRYPTOMINISAT=$cryptominisat"
-[ $drat2er != default ] \
-  && cmake_opts="$cmake_opts -DUSE_DRAT2ER=$drat2er"
 [ $glpk != default ] \
   && cmake_opts="$cmake_opts -DUSE_GLPK=$glpk"
 [ $kissat != default ] \
   && cmake_opts="$cmake_opts -DUSE_KISSAT=$kissat"
-[ $lfsc != default ] \
-  && cmake_opts="$cmake_opts -DUSE_LFSC=$lfsc"
 [ $poly != default ] \
   && cmake_opts="$cmake_opts -DUSE_POLY=$poly"
 [ $symfpu != default ] \
@@ -463,16 +432,12 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DCADICAL_DIR=$cadical_dir"
 [ "$cryptominisat_dir" != default ] \
   && cmake_opts="$cmake_opts -DCRYPTOMINISAT_DIR=$cryptominisat_dir"
-[ "$drat2er_dir" != default ] \
-  && cmake_opts="$cmake_opts -DDRAT2ER_DIR=$drat2er_dir"
 [ "$glpk_dir" != default ] \
   && cmake_opts="$cmake_opts -DGLPK_DIR=$glpk_dir"
 [ "$gmp_dir" != default ] \
   && cmake_opts="$cmake_opts -DGMP_DIR=$gmp_dir"
 [ "$kissat_dir" != default ] \
   && cmake_opts="$cmake_opts -DKISSAT=$kissat_dir"
-[ "$lfsc_dir" != default ] \
-  && cmake_opts="$cmake_opts -DLFSC_DIR=$lfsc_dir"
 [ "$poly_dir" != default ] \
   && cmake_opts="$cmake_opts -DPOLY_DIR=$poly_dir"
 [ "$symfpu_dir" != default ] \
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 5b7c1d8f8..44ba4e261 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1139,18 +1139,10 @@ if(USE_KISSAT)
   target_link_libraries(cvc4 ${Kissat_LIBRARIES})
   target_include_directories(cvc4 PRIVATE ${Kissat_INCLUDE_DIR})
 endif()
-if(USE_DRAT2ER)
-  target_link_libraries(cvc4 ${Drat2Er_LIBRARIES})
-  target_include_directories(cvc4 PRIVATE ${Drat2Er_INCLUDE_DIR})
-endif()
 if(USE_GLPK)
   target_link_libraries(cvc4 ${GLPK_LIBRARIES})
   target_include_directories(cvc4 PRIVATE ${GLPK_INCLUDE_DIR})
 endif()
-if(USE_LFSC)
-  target_link_libraries(cvc4 ${LFSC_LIBRARIES})
-  target_include_directories(cvc4 PRIVATE ${LFSC_INCLUDE_DIR})
-endif()
 if(USE_POLY)
   target_link_libraries(cvc4 ${POLY_LIBRARIES})
   target_include_directories(cvc4 PRIVATE ${POLY_INCLUDE_DIR})
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index f452c7a5c..39284227a 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -66,10 +66,6 @@ bool Configuration::isAssertionBuild() {
   return IS_ASSERTIONS_BUILD;
 }
 
-bool Configuration::isProofBuild() {
-  return IS_PROOFS_BUILD;
-}
-
 bool Configuration::isCoverageBuild() {
   return IS_COVERAGE_BUILD;
 }
@@ -144,8 +140,7 @@ std::string Configuration::copyright() {
      << "See licenses/antlr3-LICENSE for copyright and licensing information."
      << "\n\n";
 
-  if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithLfsc()
-      || Configuration::isBuiltWithCadical()
+  if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithCadical()
       || Configuration::isBuiltWithCryptominisat()
       || Configuration::isBuiltWithKissat()
       || Configuration::isBuiltWithSymFPU()
@@ -158,11 +153,6 @@ std::string Configuration::copyright() {
          << "  See http://bitbucket.org/alanmi/abc for copyright and\n"
          << "  licensing information.\n\n";
     }
-    if (Configuration::isBuiltWithLfsc()) {
-      ss << "  LFSC Proof Checker\n"
-         << "  See http://github.com/CVC4/LFSC for copyright and\n"
-         << "  licensing information.\n\n";
-    }
     if (Configuration::isBuiltWithCadical())
     {
       ss << "  CaDiCaL - Simplified Satisfiability Solver\n"
@@ -282,14 +272,8 @@ bool Configuration::isBuiltWithCryptominisat() {
 
 bool Configuration::isBuiltWithKissat() { return IS_KISSAT_BUILD; }
 
-bool Configuration::isBuiltWithDrat2Er() { return IS_DRAT2ER_BUILD; }
-
 bool Configuration::isBuiltWithEditline() { return IS_EDITLINE_BUILD; }
 
-bool Configuration::isBuiltWithLfsc() {
-  return IS_LFSC_BUILD;
-}
-
 bool Configuration::isBuiltWithPoly()
 {
   return IS_POLY_BUILD;
diff --git a/src/base/configuration.h b/src/base/configuration.h
index aab136374..ec8cc879b 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -58,8 +58,6 @@ public:
 
   static bool isAssertionBuild();
 
-  static bool isProofBuild();
-
   static bool isCoverageBuild();
 
   static bool isProfilingBuild();
@@ -106,12 +104,8 @@ public:
 
   static bool isBuiltWithKissat();
 
-  static bool isBuiltWithDrat2Er();
-
   static bool isBuiltWithEditline();
 
-  static bool isBuiltWithLfsc();
-
   static bool isBuiltWithPoly();
 
   static bool isBuiltWithSymFPU();
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index 835a02a44..cc1983734 100644
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -60,12 +60,6 @@ namespace CVC4 {
 #  define IS_ASSERTIONS_BUILD false
 #endif /* CVC4_ASSERTIONS */
 
-#ifdef CVC4_PROOF
-#  define IS_PROOFS_BUILD true
-#else  /* CVC4_PROOF */
-#  define IS_PROOFS_BUILD false
-#endif /* CVC4_PROOF */
-
 #ifdef CVC4_COVERAGE
 #  define IS_COVERAGE_BUILD true
 #else /* CVC4_COVERAGE */
@@ -120,24 +114,12 @@ namespace CVC4 {
 #  define IS_CRYPTOMINISAT_BUILD false
 #endif /* CVC4_USE_CRYPTOMINISAT */
 
-#if CVC4_USE_DRAT2ER
-#  define IS_DRAT2ER_BUILD true
-#else /* CVC4_USE_DRAT2ER */
-#  define IS_DRAT2ER_BUILD false
-#endif /* CVC4_USE_DRAT2ER */
-
 #if CVC4_USE_KISSAT
 #define IS_KISSAT_BUILD true
 #else /* CVC4_USE_KISSAT */
 #define IS_KISSAT_BUILD false
 #endif /* CVC4_USE_KISSAT */
 
-#if CVC4_USE_LFSC
-#define IS_LFSC_BUILD true
-#else /* CVC4_USE_LFSC */
-#define IS_LFSC_BUILD false
-#endif /* CVC4_USE_LFSC */
-
 #if CVC4_USE_POLY
 #define IS_POLY_BUILD true
 #else /* CVC4_USE_POLY */
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index b1cbca05b..ee3242067 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -253,36 +253,6 @@ void OptionsHandler::setProduceAssertions(std::string option, bool value)
   options::interactiveMode.set(value);
 }
 
-void OptionsHandler::proofEnabledBuild(std::string option, bool value)
-{
-#ifdef CVC4_PROOF
-  if (value && options::bitblastMode() == options::BitblastMode::EAGER
-      && options::bvSatSolver() != options::SatSolverMode::MINISAT
-      && options::bvSatSolver() != options::SatSolverMode::CRYPTOMINISAT)
-  {
-    throw OptionException(
-        "Eager BV proofs only supported when MiniSat or CryptoMiniSat is used");
-  }
-#else
-  if(value) {
-    std::stringstream ss;
-    ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support";
-    throw OptionException(ss.str());
-  }
-#endif /* CVC4_PROOF */
-}
-
-void OptionsHandler::LFSCEnabledBuild(std::string option, bool value) {
-#ifndef CVC4_USE_LFSC
-  if (value) {
-    std::stringstream ss;
-    ss << "option `" << option << "' requires a build of CVC4 with integrated "
-                                  "LFSC; this binary was not built with LFSC";
-    throw OptionException(ss.str());
-  }
-#endif /* CVC4_USE_LFSC */
-}
-
 void OptionsHandler::statsEnabledBuild(std::string option, bool value)
 {
 #ifndef CVC4_STATISTICS_ON
@@ -347,7 +317,7 @@ void OptionsHandler::showConfiguration(std::string option) {
   } else {
     print_config_cond("scm", false);
   }
-  
+
   std::cout << std::endl;
 
   std::stringstream ss;
@@ -355,7 +325,7 @@ void OptionsHandler::showConfiguration(std::string option) {
      << Configuration::getVersionMinor() << "."
      << Configuration::getVersionRelease();
   print_config("library", ss.str());
-  
+
   std::cout << std::endl;
 
   print_config_cond("debug code", Configuration::isDebugBuild());
@@ -364,29 +334,26 @@ void OptionsHandler::showConfiguration(std::string option) {
   print_config_cond("dumping", Configuration::isDumpingBuild());
   print_config_cond("muzzled", Configuration::isMuzzledBuild());
   print_config_cond("assertions", Configuration::isAssertionBuild());
-  print_config_cond("proof", Configuration::isProofBuild());
   print_config_cond("coverage", Configuration::isCoverageBuild());
   print_config_cond("profiling", Configuration::isProfilingBuild());
   print_config_cond("asan", Configuration::isAsanBuild());
   print_config_cond("ubsan", Configuration::isUbsanBuild());
   print_config_cond("tsan", Configuration::isTsanBuild());
   print_config_cond("competition", Configuration::isCompetitionBuild());
-  
+
   std::cout << std::endl;
-  
+
   print_config_cond("abc", Configuration::isBuiltWithAbc());
   print_config_cond("cln", Configuration::isBuiltWithCln());
   print_config_cond("glpk", Configuration::isBuiltWithGlpk());
   print_config_cond("cadical", Configuration::isBuiltWithCadical());
   print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat());
-  print_config_cond("drat2er", Configuration::isBuiltWithDrat2Er());
   print_config_cond("gmp", Configuration::isBuiltWithGmp());
   print_config_cond("kissat", Configuration::isBuiltWithKissat());
-  print_config_cond("lfsc", Configuration::isBuiltWithLfsc());
   print_config_cond("poly", Configuration::isBuiltWithPoly());
   print_config_cond("editline", Configuration::isBuiltWithEditline());
   print_config_cond("symfpu", Configuration::isBuiltWithSymFPU());
-  
+
   exit(0);
 }
 
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 18e8a917a..b24fb032f 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -86,8 +86,6 @@ public:
    * initialization.
    */
   void setProduceAssertions(std::string option, bool value);
-  void proofEnabledBuild(std::string option, bool value);
-  void LFSCEnabledBuild(std::string option, bool value);
 
   void statsEnabledBuild(std::string option, bool value);
 
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 787a60e78..2d678ec2b 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -198,7 +198,6 @@ header = "options/smt_options.h"
   category   = "regular"
   long       = "produce-unsat-cores"
   type       = "bool"
-  predicates = ["proofEnabledBuild"]
   help       = "turn on unsat core generation"
 
 [[option]]
@@ -238,7 +237,6 @@ header = "options/smt_options.h"
   long       = "produce-unsat-assumptions"
   type       = "bool"
   default    = "false"
-  predicates = ["proofEnabledBuild"]
   read_only  = true
   help       = "turn on unsat assumptions generation"
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4f4d983c5..f10439156 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -150,9 +150,7 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
   // d_proofManager must be created before Options has been finished
   // being parsed from the input file. Because of this, we cannot trust
   // that options::unsatCores() is set correctly yet.
-#ifdef CVC4_PROOF
   d_proofManager.reset(new ProofManager(getUserContext()));
-#endif
 
   d_definedFunctions = new (true) DefinedFunctionMap(getUserContext());
 }
@@ -331,9 +329,7 @@ SmtEngine::~SmtEngine()
     // Note: the proof manager must be destroyed before the theory engine.
     // Because the destruction of the proofs depends on contexts owned be the
     // theory solvers.
-#ifdef CVC4_PROOF
     d_proofManager.reset(nullptr);
-#endif
     d_pfManager.reset(nullptr);
     d_ucManager.reset(nullptr);
 
@@ -1406,7 +1402,6 @@ StatisticsRegistry* SmtEngine::getStatisticsRegistry()
 
 UnsatCore SmtEngine::getUnsatCoreInternal()
 {
-#if IS_PROOFS_BUILD
   if (!options::unsatCores())
   {
     throw ModalException(
@@ -1433,11 +1428,6 @@ UnsatCore SmtEngine::getUnsatCoreInternal()
   std::vector<Node> core;
   d_ucManager->getUnsatCore(pfn, *d_asserts, core);
   return UnsatCore(core);
-#else  /* IS_PROOFS_BUILD */
-  throw ModalException(
-      "This build of CVC4 doesn't have proof support (required for unsat "
-      "cores).");
-#endif /* IS_PROOFS_BUILD */
 }
 
 void SmtEngine::checkUnsatCore() {
@@ -1539,7 +1529,6 @@ std::string SmtEngine::getProof()
   {
     getPrinter().toStreamCmdGetProof(getOutputManager().getDumpOut());
   }
-#if IS_PROOFS_BUILD
   if (!options::produceProofs())
   {
     throw ModalException("Cannot get a proof when proof option is off.");
@@ -1558,9 +1547,6 @@ std::string SmtEngine::getProof()
   std::ostringstream ss;
   d_pfManager->printProof(ss, pe->getProof(), *d_asserts, *d_definedFunctions);
   return ss.str();
-#else  /* IS_PROOFS_BUILD */
-  throw ModalException("This build of CVC4 doesn't have proof support.");
-#endif /* IS_PROOFS_BUILD */
 }
 
 void SmtEngine::printInstantiations( std::ostream& out ) {
diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
index cc528f89c..2aa96dfbb 100644
--- a/src/smt/smt_engine_scope.cpp
+++ b/src/smt/smt_engine_scope.cpp
@@ -35,14 +35,8 @@ SmtEngine* currentSmtEngine() {
 bool smtEngineInScope() { return s_smtEngine_current != NULL; }
 
 ProofManager* currentProofManager() {
-#if IS_PROOFS_BUILD
   Assert(s_smtEngine_current != NULL);
   return s_smtEngine_current->getProofManager();
-#else  /* IS_PROOFS_BUILD */
-  InternalError()
-      << "proofs/unsat cores are not on, but ProofManager requested";
-  return NULL;
-#endif /* IS_PROOFS_BUILD */
 }
 
 ResourceManager* currentResourceManager()
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index 3caa1250e..35d640869 100644
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -43,7 +43,3 @@ if(ENABLE_UNIT_TESTING)
     add_subdirectory(java)
   endif()
 endif()
-
-if(LFSC_BINARY)
-  add_subdirectory(signatures)
-endif()
diff --git a/test/regress/regress0/arrays/issue3814.smt2 b/test/regress/regress0/arrays/issue3814.smt2
index 6c557d99d..6e4a41338 100644
--- a/test/regress/regress0/arrays/issue3814.smt2
+++ b/test/regress/regress0/arrays/issue3814.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: proof
 ; COMMAND-LINE: --produce-unsat-cores
 ; EXPECT: sat
 (set-logic QF_AX)
diff --git a/test/regress/regress0/bv/ackermann2.smt2 b/test/regress/regress0/bv/ackermann2.smt2
index 80b8126a0..9bba5f141 100644
--- a/test/regress/regress0/bv/ackermann2.smt2
+++ b/test/regress/regress0/bv/ackermann2.smt2
@@ -1,6 +1,5 @@
 ; COMMAND-LINE: --bitblast=eager --no-check-models  --no-check-unsat-cores
 ; REQUIRES: cryptominisat
-; REQUIRES: drat2er
 ; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_UFBV)
diff --git a/test/regress/regress0/bv/bv_to_int_5230_binary.smt2 b/test/regress/regress0/bv/bv_to_int_5230_binary.smt2
index 32680d862..406041937 100644
--- a/test/regress/regress0/bv/bv_to_int_5230_binary.smt2
+++ b/test/regress/regress0/bv/bv_to_int_5230_binary.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: proof
 ; EXPECT: sat
 (set-logic QF_UFBV)
 (set-option :produce-unsat-cores true)
diff --git a/test/regress/regress0/bv/bv_to_int_5230_missing_op.smt2 b/test/regress/regress0/bv/bv_to_int_5230_missing_op.smt2
index 757b00e5f..497fbaab1 100644
--- a/test/regress/regress0/bv/bv_to_int_5230_missing_op.smt2
+++ b/test/regress/regress0/bv/bv_to_int_5230_missing_op.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: proof
 ; EXPECT: sat
 (set-logic ABV)
 (set-option :check-unsat-cores true)
diff --git a/test/regress/regress0/bv/bv_to_int_5230_shift_const.smt2 b/test/regress/regress0/bv/bv_to_int_5230_shift_const.smt2
index e94e0cae5..a8d0144f1 100644
--- a/test/regress/regress0/bv/bv_to_int_5230_shift_const.smt2
+++ b/test/regress/regress0/bv/bv_to_int_5230_shift_const.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: proof
 ; EXPECT: sat
 (set-logic QF_UFBV)
 (set-option :check-unsat-cores true)
@@ -7,6 +6,6 @@
 (declare-const v5 Bool)
 (declare-const v8 Bool)
 (declare-const v9 Bool)
-(assert (or (distinct ((_ sign_extend 0) #b1001110) (bvlshr #b1001110 #b1001110) ((_ sign_extend 0) #b1001110) #b1001110) v9 (= #b1001110 ((_ sign_extend 0) #b1001110) #b1001110 #b1001110 ((_ sign_extend 0) #b1001110)) v5 (distinct ((_ sign_extend 0) #b1001110) (bvlshr #b1001110 #b1001110) ((_ sign_extend 0) #b1001110) #b1001110)))  
+(assert (or (distinct ((_ sign_extend 0) #b1001110) (bvlshr #b1001110 #b1001110) ((_ sign_extend 0) #b1001110) #b1001110) v9 (= #b1001110 ((_ sign_extend 0) #b1001110) #b1001110 #b1001110 ((_ sign_extend 0) #b1001110)) v5 (distinct ((_ sign_extend 0) #b1001110) (bvlshr #b1001110 #b1001110) ((_ sign_extend 0) #b1001110) #b1001110)))
 (assert (or v0 v8))
 (check-sat)
diff --git a/test/regress/regress0/bv/core/slice-12.smtv1.smt2 b/test/regress/regress0/bv/core/slice-12.smtv1.smt2
index d66b27caa..f370c0f0f 100644
--- a/test/regress/regress0/bv/core/slice-12.smtv1.smt2
+++ b/test/regress/regress0/bv/core/slice-12.smtv1.smt2
@@ -1,5 +1,4 @@
 ; REQUIRES: cryptominisat
-; REQUIRES: drat2er
 ; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --no-check-unsat-cores
 ; EXPECT: unsat
 (set-option :incremental false)
diff --git a/test/regress/regress0/dump-unsat-core-full.smt2 b/test/regress/regress0/dump-unsat-core-full.smt2
index 3c68501f9..a21508efb 100644
--- a/test/regress/regress0/dump-unsat-core-full.smt2
+++ b/test/regress/regress0/dump-unsat-core-full.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: proof
 ; COMMAND-LINE: --dump-unsat-cores-full
 ; EXPECT: unsat
 ; EXPECT: (
diff --git a/test/regress/regress0/nl/issue3959.smt2 b/test/regress/regress0/nl/issue3959.smt2
index cce64a848..eccd6b301 100644
--- a/test/regress/regress0/nl/issue3959.smt2
+++ b/test/regress/regress0/nl/issue3959.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: proof
 ; COMMAND-LINE: --produce-unsat-cores --incremental
 ; EXPECT: sat
 
diff --git a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 b/test/regress/regress1/quantifiers/dump-inst-proof.smt2
index 274fc213f..0c8c21f01 100644
--- a/test/regress/regress1/quantifiers/dump-inst-proof.smt2
+++ b/test/regress/regress1/quantifiers/dump-inst-proof.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: proof
 ; COMMAND-LINE: --dump-instantiations --produce-unsat-cores --print-inst-full
 ; EXPECT: unsat
 ; EXPECT: (instantiations (forall ((x Int)) (or (P x) (Q x)))
diff --git a/test/regress/regress1/sygus-abduct-test-ccore.smt2 b/test/regress/regress1/sygus-abduct-test-ccore.smt2
index adb38add0..86f5fe133 100644
--- a/test/regress/regress1/sygus-abduct-test-ccore.smt2
+++ b/test/regress/regress1/sygus-abduct-test-ccore.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: proof
 ; COMMAND-LINE: --produce-abducts --sygus-core-connective
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
diff --git a/test/regress/regress1/sygus-abduct-test-user.smt2 b/test/regress/regress1/sygus-abduct-test-user.smt2
index ed1d5c862..bb02ebce2 100644
--- a/test/regress/regress1/sygus-abduct-test-user.smt2
+++ b/test/regress/regress1/sygus-abduct-test-user.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: proof
 ; COMMAND-LINE: --produce-abducts
 ; COMMAND-LINE: --produce-abducts --sygus-core-connective
 ; SCRUBBER: grep -v -E '(\(define-fun)'
diff --git a/test/regress/regress1/sygus/abd-simple-conj-4.smt2 b/test/regress/regress1/sygus/abd-simple-conj-4.smt2
index dda5e9751..98bf70fd7 100644
--- a/test/regress/regress1/sygus/abd-simple-conj-4.smt2
+++ b/test/regress/regress1/sygus/abd-simple-conj-4.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: proof
 ; COMMAND-LINE: --produce-abducts --sygus-core-connective
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
diff --git a/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2 b/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2
index 691cf6d9a..1595b0865 100644
--- a/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2
+++ b/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: proof
 ; COMMAND-LINE: --produce-abducts --sygus-core-connective
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
diff --git a/test/regress/regress1/sygus/abduction_streq.readable.smt2 b/test/regress/regress1/sygus/abduction_streq.readable.smt2
index b6a422035..b466ab33e 100644
--- a/test/regress/regress1/sygus/abduction_streq.readable.smt2
+++ b/test/regress/regress1/sygus/abduction_streq.readable.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: proof
 ; COMMAND-LINE: --produce-abducts --sygus-core-connective
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
diff --git a/test/regress/regress1/sygus/array_search_2.sy b/test/regress/regress1/sygus/array_search_2.sy
index c2404a12c..9009c8260 100644
--- a/test/regress/regress1/sygus/array_search_2.sy
+++ b/test/regress/regress1/sygus/array_search_2.sy
@@ -1,4 +1,3 @@
-; REQUIRES: proof
 ; EXPECT: unsat
 ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
 (set-logic LIA)
diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index fb4786331..01924559a 100755
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -10,12 +10,6 @@
 ## directory for licensing information.
 ##
 """
-Usage:
-
-    run_regression.py [--enable-proof] [--with-lfsc] [--dump]
-        [--use-skip-return-code] [wrapper] cvc4-binary
-        [benchmark.cvc | benchmark.smt | benchmark.smt2 | benchmark.p]
-
 Runs benchmark and checks for correct exit status and output.
 """
 
@@ -193,11 +187,6 @@ def run_regression(check_unsat_cores, check_proofs, dump, use_skip_return_code,
 
     cvc4_features, cvc4_disabled_features = get_cvc4_features(cvc4_binary)
 
-    # Disable proof and unsat core checks if CVC4 was not compiled with proofs.
-    if 'proof' not in cvc4_features:
-        check_unsat_cores = False
-        check_proofs = False
-
     basic_command_line_args = []
 
     benchmark_basename = os.path.basename(benchmark_path)
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index 71568e337..f63f3f315 100644
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -40,10 +40,6 @@ macro(cvc4_add_unit_test is_white name output_dir)
   target_link_libraries(${name} main-test)
   target_link_libraries(${name} GTest::GTest)
   target_link_libraries(${name} GTest::Main)
-  if(USE_LFSC)
-    # We don't link against LFSC, because CVC4 is already linked against it.
-    target_include_directories(${name} PRIVATE ${LFSC_INCLUDE_DIR})
-  endif()
   if(USE_POLY)
     # We don't link against libpoly, because CVC4 is already linked against it.
     target_include_directories(${name} PRIVATE ${POLY_INCLUDE_DIR})
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 18a8f9cc8..6b6a0fa0f 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -1346,59 +1346,48 @@ TEST_F(TestApiBlackSolver, getOption)
 
 TEST_F(TestApiBlackSolver, getUnsatAssumptions1)
 {
-#if IS_PROOFS_BUILD
   d_solver.setOption("incremental", "false");
   d_solver.checkSatAssuming(d_solver.mkFalse());
   ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC4ApiException);
-#endif
 }
 
 TEST_F(TestApiBlackSolver, getUnsatAssumptions2)
 {
-#if IS_PROOFS_BUILD
   d_solver.setOption("incremental", "true");
   d_solver.setOption("produce-unsat-assumptions", "false");
   d_solver.checkSatAssuming(d_solver.mkFalse());
   ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC4ApiException);
-#endif
 }
 
 TEST_F(TestApiBlackSolver, getUnsatAssumptions3)
 {
-#if IS_PROOFS_BUILD
   d_solver.setOption("incremental", "true");
   d_solver.setOption("produce-unsat-assumptions", "true");
   d_solver.checkSatAssuming(d_solver.mkFalse());
   ASSERT_NO_THROW(d_solver.getUnsatAssumptions());
   d_solver.checkSatAssuming(d_solver.mkTrue());
   ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC4ApiException);
-#endif
 }
 
 TEST_F(TestApiBlackSolver, getUnsatCore1)
 {
-#if IS_PROOFS_BUILD
   d_solver.setOption("incremental", "false");
   d_solver.assertFormula(d_solver.mkFalse());
   d_solver.checkSat();
   ASSERT_THROW(d_solver.getUnsatCore(), CVC4ApiException);
-#endif
 }
 
 TEST_F(TestApiBlackSolver, getUnsatCore2)
 {
-#if IS_PROOFS_BUILD
   d_solver.setOption("incremental", "false");
   d_solver.setOption("produce-unsat-cores", "false");
   d_solver.assertFormula(d_solver.mkFalse());
   d_solver.checkSat();
   ASSERT_THROW(d_solver.getUnsatCore(), CVC4ApiException);
-#endif
 }
 
 TEST_F(TestApiBlackSolver, getUnsatCore3)
 {
-#if IS_PROOFS_BUILD
   d_solver.setOption("incremental", "true");
   d_solver.setOption("produce-unsat-cores", "true");
 
@@ -1434,9 +1423,8 @@ TEST_F(TestApiBlackSolver, getUnsatCore3)
   {
     d_solver.assertFormula(t);
   }
-  Result res = d_solver.checkSat();
+  CVC4::api::Result res = d_solver.checkSat();
   ASSERT_TRUE(res.isUnsat());
-#endif
 }
 
 TEST_F(TestApiBlackSolver, getValue1)