Index index by Group index by Distribution index by Vendor index by creation date index by Name Mirrors Help Search

cvc4-debugsource-1.8-13.fc37 RPM for x86_64

From Fedora 37 updates for x86_64 / debug / Packages / c

Name: cvc4-debugsource Distribution: Fedora Project
Version: 1.8 Vendor: Fedora Project
Release: 13.fc37 Build date: Tue Oct 11 23:41:38 2022
Group: Development/Debug Build host: buildvm-x86-07.iad2.fedoraproject.org
Size: 25203557 Source RPM: cvc4-1.8-13.fc37.src.rpm
Packager: Fedora Project
Url: https://cvc4.github.io/
Summary: Debug sources for package cvc4
 
This package provides debug sources for package cvc4.
Debug sources are useful when developing applications that use this
package or when debugging this package.

Provides

Requires

License

BSD-3-Clause AND MIT

Changelog

* Tue Oct 11 2022 Jerry James <loganjerry@gmail.com> - 1.8-13
  - Add -bash-patsub-replacement patch to fix build with bash 5.2 (bz 2133760)
  - Add -toml patch and drop python3-toml BR
* Mon Aug 15 2022 Jerry James <loganjerry@gmail.com> - 1.8-12
  - Convert License tag to SPDX
* Wed Jul 20 2022 Fedora Release Engineering <releng@fedoraproject.org> - 1.8-12
  - Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild
* Tue Jul 19 2022 Jerry James <loganjerry@gmail.com> - 1.8-11
  - Drop support for i686 due to ANTLR unavailability
* Mon Jun 13 2022 Python Maint <python-maint@redhat.com> - 1.8-11
  - Rebuilt for Python 3.11
* Fri Mar 04 2022 Jerry James <loganjerry@gmail.com> - 1.8-10
  - Remove . from %cmake invocation to fix FTBFS (rhbz#2060821)
  - Drop -const-map-key patch now that gcc has been fixed
* Sat Feb 05 2022 Jiri Vanek <jvanek@redhat.com> - 1.8-9
  - Rebuilt for java-17-openjdk as system jdk
* Sat Jan 22 2022 Jerry James <loganjerry@gmail.com> - 1.8-8
  - Add -const-map-key patch to fix FTBFS
* Thu Jan 20 2022 Fedora Release Engineering <releng@fedoraproject.org> - 1.8-8
  - Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild
  - Use the default linker
* Wed Jul 21 2021 Fedora Release Engineering <releng@fedoraproject.org> - 1.8-7
  - Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
* Fri Jun 04 2021 Python Maint <python-maint@redhat.com> - 1.8-6
  - Rebuilt for Python 3.10
* Wed Jun 02 2021 Jerry James <loganjerry@gmail.com> - 1.8-5
  - Remove spurious rpaths (bz 1967190)
  - Fix broken jar symlink
  - Add missing executable bit to python shared object
* Tue Jan 26 2021 Fedora Release Engineering <releng@fedoraproject.org> - 1.8-4
  - Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild
* Wed Jan 20 2021 Jerry James <loganjerry@gamil.com> - 1.8-3
  - Add -dup-decl patch to fix FTBFS with recent LFSC versions
* Fri Nov 27 2020 Jerry James <loganjerry@gmail.com> - 1.8-2
  - Rebuild for cryptominisat 5.8.0

Files

/usr/src/debug/cvc4-1.8-13.fc37.x86_64
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/proofs
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/proofs/signatures
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/proofs/signatures/signatures.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/api
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/api/python
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/api/python/pycvc4.cxx
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/base
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/base/git_versioninfo.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/bindings
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/bindings/java
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/bindings/java/CMakeFiles
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/bindings/java/CMakeFiles/cvc4jni.dir
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/bindings/java/CMakeFiles/cvc4jni.dir/cvc4JAVA_wrap.cxx
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/bindings/python
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/bindings/python/CMakeFiles
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/bindings/python/CMakeFiles/_CVC4.dir
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/bindings/python/CMakeFiles/_CVC4.dir/cvc4PYTHON_wrap.cxx
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/expr
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/expr/expr.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/expr/expr_manager.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/expr/kind.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/expr/kind.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/expr/metakind.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/expr/metakind.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/expr/type_checker.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/main
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/arith_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/arith_options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/arrays_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/arrays_options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/base_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/base_options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/booleans_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/builtin_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/bv_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/bv_options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/datatypes_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/datatypes_options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/decision_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/decision_options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/expr_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/expr_options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/fp_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/fp_options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/main_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/main_options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/options_holder.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/parser_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/parser_options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/printer_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/printer_options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/proof_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/proof_options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/prop_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/prop_options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/quantifiers_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/quantifiers_options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/sep_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/sep_options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/sets_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/sets_options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/smt_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/smt_options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/strings_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/strings_options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/theory_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/theory_options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/uf_options.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/options/uf_options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/parser
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/parser/cvc
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/parser/cvc/CvcLexer.c
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/parser/cvc/CvcLexer.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/parser/cvc/CvcParser.c
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/parser/cvc/CvcParser.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/parser/smt2
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/parser/smt2/Smt2Lexer.c
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/parser/smt2/Smt2Lexer.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/parser/smt2/Smt2Parser.c
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/parser/smt2/Smt2Parser.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/parser/tptp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/parser/tptp/TptpLexer.c
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/parser/tptp/TptpLexer.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/parser/tptp/TptpParser.c
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/parser/tptp/TptpParser.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/theory
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/theory/rewriter_tables.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/theory/type_enumerator.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/util
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/redhat-linux-build/src/util/floatingpoint.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/api
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/api/cvc4cpp.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/api/cvc4cpp.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/api/cvc4cppkind.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/base
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/base/check.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/base/check.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/base/configuration.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/base/configuration.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/base/exception.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/base/exception.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/base/listener.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/base/listener.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/base/map_util.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/base/modal_exception.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/base/output.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/base/output.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/bindings
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/bindings/java_iterator_adapter.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/bindings/java_stream_adapters.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/context
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/context/backtrackable.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/context/cdhashmap.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/context/cdhashmap_forward.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/context/cdhashset.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/context/cdinsert_hashmap.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/context/cdinsert_hashmap_forward.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/context/cdlist.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/context/cdlist_forward.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/context/cdmaybe.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/context/cdo.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/context/cdqueue.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/context/cdtrail_queue.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/context/context.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/context/context.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/context/context_mm.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/context/context_mm.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/decision
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/decision/decision_attributes.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/decision/decision_engine.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/decision/decision_engine.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/decision/decision_strategy.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/decision/justification_heuristic.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/decision/justification_heuristic.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/array_store_all.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/array_store_all.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/ascription_type.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/attribute.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/attribute.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/attribute_internals.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/attribute_unique_id.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/datatype.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/datatype.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/dtype.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/dtype.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/dtype_cons.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/dtype_cons.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/dtype_selector.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/dtype_selector.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/emptyset.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/emptyset.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/expr_iomanip.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/expr_iomanip.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/expr_manager_scope.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/expr_manager_template.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/expr_manager_template.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/expr_sequence.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/expr_sequence.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/expr_template.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/expr_template.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/kind_map.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/kind_template.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/kind_template.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/lazy_proof.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/lazy_proof.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/match_trie.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/match_trie.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/node.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/node.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/node_algorithm.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/node_algorithm.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/node_builder.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/node_manager.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/node_manager.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/node_manager_attributes.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/node_manager_listeners.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/node_manager_listeners.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/node_self_iterator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/node_traversal.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/node_traversal.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/node_trie.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/node_trie.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/node_value.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/node_value.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/node_visitor.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/proof.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/proof.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/proof_checker.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/proof_checker.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/proof_generator.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/proof_generator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/proof_node.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/proof_node.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/proof_node_algorithm.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/proof_node_algorithm.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/proof_node_manager.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/proof_node_manager.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/proof_node_to_sexpr.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/proof_node_to_sexpr.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/proof_rule.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/proof_rule.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/proof_step_buffer.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/proof_step_buffer.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/record.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/record.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/sequence.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/sequence.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/skolem_manager.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/skolem_manager.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/sygus_datatype.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/sygus_datatype.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/symbol_table.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/symbol_table.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/term_canonize.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/term_canonize.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/term_conversion_proof_generator.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/term_conversion_proof_generator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/type.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/type.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/type_checker.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/type_checker_template.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/type_checker_util.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/type_matcher.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/type_matcher.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/type_node.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/type_node.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/type_properties_template.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/uninterpreted_constant.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/uninterpreted_constant.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/expr/variable_type_map.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/lib
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/lib/clock_gettime.c
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/lib/ffs.c
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/lib/strtok_r.c
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/main
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/main/command_executor.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/main/command_executor.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/main/driver_unified.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/main/interactive_shell.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/main/interactive_shell.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/main/main.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/main/main.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/main/util.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/options
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/options/base_handlers.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/options/decision_weight.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/options/didyoumean.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/options/didyoumean.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/options/language.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/options/language.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/options/open_ostream.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/options/open_ostream.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/options/option_exception.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/options/option_exception.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/options/options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/options/options_handler.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/options/options_handler.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/options/options_public_functions.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/options/printer_modes.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/options/printer_modes.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/options/set_language.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/options/set_language.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/antlr_input.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/antlr_input.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/antlr_input_imports.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/antlr_line_buffered_input.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/antlr_line_buffered_input.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/bounded_token_buffer.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/bounded_token_buffer.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/bounded_token_factory.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/bounded_token_factory.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/cvc
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/cvc/cvc.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/cvc/cvc.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/cvc/cvc_input.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/cvc/cvc_input.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/input.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/input.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/line_buffer.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/line_buffer.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/memory_mapped_input_buffer.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/memory_mapped_input_buffer.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/parse_op.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/parse_op.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/parser.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/parser.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/parser_builder.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/parser_builder.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/parser_exception.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/smt2
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/smt2/smt2.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/smt2/smt2.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/smt2/smt2_input.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/smt2/smt2_input.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/smt2/sygus_input.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/smt2/sygus_input.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/tptp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/tptp/tptp.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/tptp/tptp.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/tptp/tptp_input.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/parser/tptp/tptp_input.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/assertion_pipeline.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/assertion_pipeline.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/ackermann.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/ackermann.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/apply_substs.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/apply_substs.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/bool_to_bv.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/bool_to_bv.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/bv_abstraction.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/bv_abstraction.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/bv_eager_atoms.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/bv_eager_atoms.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/bv_gauss.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/bv_gauss.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/bv_intro_pow2.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/bv_intro_pow2.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/bv_to_bool.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/bv_to_bool.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/bv_to_int.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/bv_to_int.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/extended_rewriter_pass.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/extended_rewriter_pass.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/global_negate.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/global_negate.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/ho_elim.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/ho_elim.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/int_to_bv.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/int_to_bv.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/ite_removal.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/ite_removal.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/ite_simp.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/ite_simp.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/miplib_trick.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/miplib_trick.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/nl_ext_purify.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/nl_ext_purify.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/non_clausal_simp.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/non_clausal_simp.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/pseudo_boolean_processor.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/pseudo_boolean_processor.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/quantifier_macros.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/quantifier_macros.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/quantifiers_preprocess.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/quantifiers_preprocess.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/real_to_int.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/real_to_int.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/rewrite.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/rewrite.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/sep_skolem_emp.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/sep_skolem_emp.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/sort_infer.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/sort_infer.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/static_learning.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/static_learning.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/sygus_inference.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/sygus_inference.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/synth_rew_rules.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/synth_rew_rules.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/theory_preprocess.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/theory_preprocess.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/unconstrained_simplifier.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/passes/unconstrained_simplifier.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/preprocessing_pass.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/preprocessing_pass.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/preprocessing_pass_context.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/preprocessing_pass_context.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/preprocessing_pass_registry.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/preprocessing_pass_registry.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/util
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/util/ite_utilities.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/preprocessing/util/ite_utilities.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/printer
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/printer/ast
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/printer/ast/ast_printer.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/printer/ast/ast_printer.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/printer/cvc
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/printer/cvc/cvc_printer.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/printer/cvc/cvc_printer.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/printer/dagification_visitor.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/printer/dagification_visitor.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/printer/printer.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/printer/printer.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/printer/smt2
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/printer/smt2/smt2_printer.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/printer/smt2/smt2_printer.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/printer/sygus_print_callback.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/printer/sygus_print_callback.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/printer/tptp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/printer/tptp/tptp_printer.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/printer/tptp/tptp_printer.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/arith_proof.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/arith_proof.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/arith_proof_recorder.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/arith_proof_recorder.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/array_proof.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/array_proof.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/bitvector_proof.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/bitvector_proof.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/clausal_bitvector_proof.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/clausal_bitvector_proof.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/clause_id.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/cnf_proof.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/cnf_proof.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/dimacs.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/dimacs.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/drat
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/drat/drat_proof.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/drat/drat_proof.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/er
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/er/er_proof.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/er/er_proof.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/lemma_proof.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/lemma_proof.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/lfsc_proof_printer.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/lfsc_proof_printer.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/lrat
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/lrat/lrat_proof.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/lrat/lrat_proof.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/proof_manager.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/proof_manager.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/proof_output_channel.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/proof_output_channel.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/proof_utils.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/proof_utils.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/resolution_bitvector_proof.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/resolution_bitvector_proof.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/sat_proof.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/sat_proof_implementation.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/simplify_boolean_node.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/simplify_boolean_node.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/skolemization_manager.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/skolemization_manager.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/theory_proof.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/theory_proof.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/uf_proof.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/uf_proof.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/unsat_core.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/proof/unsat_core.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bv_sat_solver_notify.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat/bvminisat.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat/bvminisat.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat/core
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat/core/Solver.cc
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat/core/Solver.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat/core/SolverTypes.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat/mtl
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat/mtl/Alg.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat/mtl/Alloc.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat/mtl/Heap.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat/mtl/Map.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat/mtl/Queue.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat/mtl/Sort.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat/mtl/Vec.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat/mtl/XAlloc.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat/simp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat/simp/SimpSolver.cc
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat/simp/SimpSolver.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat/utils
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat/utils/Options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/bvminisat/utils/ParseUtils.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/cadical.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/cadical.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/cnf_stream.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/cnf_stream.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/cryptominisat.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/cryptominisat.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/kissat.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/kissat.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat/core
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat/core/Solver.cc
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat/core/Solver.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat/core/SolverTypes.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat/minisat.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat/minisat.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat/mtl
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat/mtl/Alg.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat/mtl/Alloc.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat/mtl/Heap.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat/mtl/Map.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat/mtl/Queue.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat/mtl/Sort.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat/mtl/Vec.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat/mtl/XAlloc.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat/simp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat/simp/SimpSolver.cc
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat/simp/SimpSolver.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat/utils
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat/utils/Options.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/minisat/utils/ParseUtils.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/prop_engine.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/prop_engine.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/registrar.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/sat_solver.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/sat_solver_factory.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/sat_solver_factory.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/sat_solver_types.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/sat_solver_types.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/theory_proxy.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/prop/theory_proxy.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/command.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/command.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/command_list.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/command_list.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/defined_function.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/dump.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/dump.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/logic_exception.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/logic_request.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/logic_request.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/managed_ostreams.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/managed_ostreams.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/model.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/model.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/model_blocker.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/model_blocker.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/model_core_builder.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/model_core_builder.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/process_assertions.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/process_assertions.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/set_defaults.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/set_defaults.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/smt_engine.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/smt_engine.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/smt_engine_scope.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/smt_engine_scope.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/smt_engine_stats.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/smt_engine_stats.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/smt_statistics_registry.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/smt_statistics_registry.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/term_formula_removal.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/term_formula_removal.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt/update_ostream.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt_util
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt_util/boolean_simplification.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt_util/boolean_simplification.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt_util/nary_builder.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/smt_util/nary_builder.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/approx_simplex.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/approx_simplex.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/arith_ite_utils.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/arith_ite_utils.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/arith_msum.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/arith_msum.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/arith_rewriter.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/arith_rewriter.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/arith_static_learner.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/arith_static_learner.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/arith_utilities.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/arith_utilities.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/arithvar.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/arithvar.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/attempt_solution_simplex.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/attempt_solution_simplex.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/bound_counts.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/callbacks.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/callbacks.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/congruence_manager.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/congruence_manager.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/constraint.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/constraint.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/constraint_forward.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/cut_log.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/cut_log.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/delta_rational.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/delta_rational.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/dio_solver.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/dio_solver.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/dual_simplex.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/dual_simplex.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/error_set.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/error_set.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/fc_simplex.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/fc_simplex.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/infer_bounds.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/infer_bounds.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/kinds
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/linear_equality.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/linear_equality.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/matrix.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/matrix.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/nl
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/nl/nl_constraint.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/nl/nl_constraint.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/nl/nl_lemma_utils.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/nl/nl_lemma_utils.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/nl/nl_model.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/nl/nl_model.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/nl/nl_monomial.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/nl/nl_monomial.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/nl/nl_solver.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/nl/nl_solver.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/nl/nonlinear_extension.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/nl/nonlinear_extension.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/nl/transcendental_solver.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/nl/transcendental_solver.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/normal_form.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/normal_form.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/partial_model.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/partial_model.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/simplex.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/simplex.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/simplex_update.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/simplex_update.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/soi_simplex.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/soi_simplex.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/tableau.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/tableau.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/tableau_sizes.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/tableau_sizes.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/theory_arith.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/theory_arith.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/theory_arith_private.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/theory_arith_private.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/theory_arith_type_rules.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arith/type_enumerator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arrays
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arrays/array_info.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arrays/array_info.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arrays/array_proof_reconstruction.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arrays/array_proof_reconstruction.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arrays/kinds
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arrays/static_fact_manager.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arrays/static_fact_manager.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arrays/theory_arrays.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arrays/theory_arrays.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arrays/theory_arrays_rewriter.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arrays/theory_arrays_rewriter.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arrays/theory_arrays_type_rules.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arrays/type_enumerator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arrays/union_find.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/arrays/union_find.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/assertion.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/assertion.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/atom_requests.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/atom_requests.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/booleans
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/booleans/circuit_propagator.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/booleans/circuit_propagator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/booleans/kinds
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/booleans/proof_checker.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/booleans/proof_checker.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/booleans/theory_bool.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/booleans/theory_bool.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/booleans/theory_bool_rewriter.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/booleans/theory_bool_rewriter.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/booleans/theory_bool_type_rules.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/booleans/type_enumerator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/builtin
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/builtin/kinds
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/builtin/proof_checker.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/builtin/proof_checker.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/builtin/theory_builtin.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/builtin/theory_builtin.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/builtin/theory_builtin_rewriter.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/builtin/theory_builtin_rewriter.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/builtin/theory_builtin_type_rules.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/builtin/type_enumerator.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/builtin/type_enumerator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/abstraction.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/abstraction.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bitblast
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bitblast/aig_bitblaster.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bitblast/aig_bitblaster.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bitblast/bitblast_strategies_template.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bitblast/bitblast_utils.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bitblast/bitblaster.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bitblast/eager_bitblaster.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bitblast/eager_bitblaster.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bitblast/lazy_bitblaster.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bitblast/lazy_bitblaster.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bv_eager_solver.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bv_eager_solver.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bv_inequality_graph.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bv_inequality_graph.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bv_quick_check.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bv_quick_check.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bv_subtheory.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bv_subtheory_algebraic.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bv_subtheory_algebraic.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bv_subtheory_bitblast.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bv_subtheory_bitblast.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bv_subtheory_core.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bv_subtheory_core.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bv_subtheory_inequality.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/bv_subtheory_inequality.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/kinds
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/slicer.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/slicer.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/theory_bv.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/theory_bv.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/theory_bv_rewrite_rules.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/theory_bv_rewrite_rules_core.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/theory_bv_rewrite_rules_normalization.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/theory_bv_rewrite_rules_simplification.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/theory_bv_rewriter.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/theory_bv_rewriter.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/theory_bv_type_rules.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/theory_bv_utils.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/theory_bv_utils.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/bv/type_enumerator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/care_graph.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/datatypes
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/datatypes/datatypes_rewriter.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/datatypes/datatypes_rewriter.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/datatypes/kinds
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/datatypes/sygus_datatype_utils.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/datatypes/sygus_datatype_utils.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/datatypes/sygus_extension.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/datatypes/sygus_extension.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/datatypes/sygus_simple_sym.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/datatypes/sygus_simple_sym.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/datatypes/theory_datatypes.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/datatypes/theory_datatypes.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/datatypes/theory_datatypes_type_rules.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/datatypes/theory_datatypes_utils.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/datatypes/theory_datatypes_utils.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/datatypes/type_enumerator.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/datatypes/type_enumerator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/decision_manager.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/decision_manager.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/decision_strategy.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/decision_strategy.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/eager_proof_generator.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/eager_proof_generator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/engine_output_channel.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/engine_output_channel.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/evaluator.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/evaluator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/ext_theory.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/ext_theory.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/fp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/fp/fp_converter.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/fp/fp_converter.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/fp/kinds
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/fp/theory_fp.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/fp/theory_fp.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/fp/theory_fp_rewriter.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/fp/theory_fp_rewriter.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/fp/theory_fp_type_rules.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/fp/type_enumerator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/interrupted.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/logic_info.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/logic_info.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/output_channel.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/alpha_equivalence.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/alpha_equivalence.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/anti_skolem.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/anti_skolem.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/bv_inverter.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/bv_inverter.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/bv_inverter_utils.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/bv_inverter_utils.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/candidate_rewrite_database.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/candidate_rewrite_database.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/candidate_rewrite_filter.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/candidate_rewrite_filter.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/cegqi
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/cegqi/ceg_instantiator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/cegqi/vts_term_cache.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/cegqi/vts_term_cache.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/conjecture_generator.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/conjecture_generator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/dynamic_rewrite.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/dynamic_rewrite.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/ematching
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/ematching/candidate_generator.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/ematching/candidate_generator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/ematching/ho_trigger.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/ematching/ho_trigger.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/ematching/inst_match_generator.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/ematching/inst_match_generator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/ematching/instantiation_engine.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/ematching/instantiation_engine.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/ematching/trigger.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/ematching/trigger.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/equality_infer.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/equality_infer.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/equality_query.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/equality_query.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/expr_miner.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/expr_miner.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/expr_miner_manager.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/expr_miner_manager.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/extended_rewrite.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/extended_rewrite.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/first_order_model.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/first_order_model.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/fmf
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/fmf/bounded_integers.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/fmf/bounded_integers.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/fmf/full_model_check.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/fmf/full_model_check.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/fmf/model_builder.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/fmf/model_builder.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/fmf/model_engine.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/fmf/model_engine.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/fun_def_evaluator.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/fun_def_evaluator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/fun_def_process.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/fun_def_process.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/inst_match.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/inst_match.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/inst_match_trie.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/inst_match_trie.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/inst_strategy_enumerative.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/inst_strategy_enumerative.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/instantiate.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/instantiate.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/kinds
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/lazy_trie.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/lazy_trie.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/proof_checker.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/proof_checker.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/quant_conflict_find.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/quant_conflict_find.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/quant_epr.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/quant_epr.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/quant_relevance.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/quant_relevance.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/quant_rep_bound_ext.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/quant_rep_bound_ext.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/quant_split.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/quant_split.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/quant_util.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/quant_util.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/quantifiers_attributes.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/quantifiers_attributes.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/quantifiers_rewriter.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/quantifiers_rewriter.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/query_generator.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/query_generator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/relevant_domain.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/relevant_domain.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/single_inv_partition.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/single_inv_partition.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/skolemize.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/skolemize.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/solution_filter.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/solution_filter.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/ce_guided_single_inv.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/cegis.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/cegis.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/cegis_core_connective.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/cegis_core_connective.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/cegis_unif.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/cegis_unif.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/enum_stream_substitution.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/example_eval_cache.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/example_eval_cache.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/example_infer.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/example_infer.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/example_min_eval.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/example_min_eval.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_abduct.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_abduct.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_enumerator.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_enumerator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_enumerator_basic.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_eval_unfold.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_explain.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_explain.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_grammar_cons.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_grammar_norm.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_grammar_red.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_invariance.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_invariance.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_module.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_module.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_pbe.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_pbe.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_process_conj.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_process_conj.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_repair_const.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_repair_const.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_stats.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_stats.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_unif.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_unif.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_unif_io.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_unif_io.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_unif_rl.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/sygus_unif_strat.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/synth_conjecture.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/synth_conjecture.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/synth_engine.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/synth_engine.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/term_database_sygus.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/term_database_sygus.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/transition_inference.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/transition_inference.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/type_info.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/type_info.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/type_node_id_trie.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus/type_node_id_trie.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus_inst.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus_inst.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus_sampler.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/sygus_sampler.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/term_database.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/term_database.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/term_enumeration.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/term_enumeration.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/term_util.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/term_util.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/theory_quantifiers.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/theory_quantifiers.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers/theory_quantifiers_type_rules.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers_engine.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/quantifiers_engine.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/rep_set.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/rep_set.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/rewriter.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/rewriter.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/rewriter_attributes.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sep
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sep/kinds
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sep/theory_sep.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sep/theory_sep.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sep/theory_sep_rewriter.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sep/theory_sep_rewriter.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sep/theory_sep_type_rules.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/cardinality_extension.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/cardinality_extension.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/inference_manager.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/inference_manager.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/kinds
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/normal_form.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/rels_utils.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/skolem_cache.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/skolem_cache.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/solver_state.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/solver_state.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/theory_sets.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/theory_sets.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/theory_sets_private.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/theory_sets_private.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/theory_sets_rels.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/theory_sets_rels.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/theory_sets_rewriter.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/theory_sets_rewriter.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/theory_sets_type_enumerator.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/theory_sets_type_enumerator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sets/theory_sets_type_rules.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/shared_terms_database.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/shared_terms_database.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/smt_engine_subsolver.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/smt_engine_subsolver.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sort_inference.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/sort_inference.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/arith_entail.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/arith_entail.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/base_solver.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/base_solver.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/core_solver.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/core_solver.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/eqc_info.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/eqc_info.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/extf_solver.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/extf_solver.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/infer_info.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/infer_info.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/inference_manager.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/inference_manager.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/kinds
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/normal_form.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/normal_form.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/regexp_elim.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/regexp_elim.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/regexp_entail.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/regexp_entail.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/regexp_operation.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/regexp_operation.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/regexp_solver.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/regexp_solver.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/rewrites.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/rewrites.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/sequences_rewriter.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/sequences_rewriter.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/sequences_stats.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/sequences_stats.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/skolem_cache.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/skolem_cache.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/solver_state.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/solver_state.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/strings_entail.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/strings_entail.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/strings_fmf.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/strings_fmf.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/strings_rewriter.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/strings_rewriter.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/term_registry.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/term_registry.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/theory_strings.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/theory_strings.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/theory_strings_preprocess.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/theory_strings_preprocess.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/theory_strings_type_rules.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/theory_strings_utils.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/theory_strings_utils.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/type_enumerator.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/type_enumerator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/word.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/strings/word.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/subs_minimize.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/subs_minimize.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/substitutions.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/substitutions.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/term_registration_visitor.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/term_registration_visitor.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/theory.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/theory.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/theory_engine.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/theory_engine.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/theory_id.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/theory_id.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/theory_model.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/theory_model.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/theory_model_builder.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/theory_model_builder.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/theory_preprocessor.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/theory_preprocessor.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/theory_proof_step_buffer.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/theory_proof_step_buffer.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/theory_registrar.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/theory_rewriter.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/theory_traits_template.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/trust_node.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/trust_node.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/type_enumerator.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/type_enumerator_template.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/type_set.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/type_set.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/uf
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/uf/cardinality_extension.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/uf/cardinality_extension.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/uf/equality_engine.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/uf/equality_engine.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/uf/equality_engine_types.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/uf/ho_extension.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/uf/ho_extension.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/uf/kinds
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/uf/proof_checker.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/uf/proof_checker.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/uf/symmetry_breaker.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/uf/symmetry_breaker.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/uf/theory_uf.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/uf/theory_uf.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/uf/theory_uf_model.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/uf/theory_uf_model.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/uf/theory_uf_rewriter.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/uf/theory_uf_type_rules.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/valuation.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/theory/valuation.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/abstract_value.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/abstract_value.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/bin_heap.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/bitvector.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/bitvector.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/bool.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/cardinality.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/cardinality.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/dense_map.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/divisible.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/divisible.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/floatingpoint.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/gmp_util.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/hash.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/index.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/index.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/integer_gmp_imp.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/integer_gmp_imp.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/maybe.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/ostream_util.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/ostream_util.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/proof.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/random.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/random.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/rational_gmp_imp.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/rational_gmp_imp.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/regexp.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/regexp.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/resource_manager.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/resource_manager.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/result.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/result.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/safe_print.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/safe_print.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/sampler.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/sampler.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/sexpr.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/sexpr.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/smt2_quote_string.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/smt2_quote_string.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/statistics.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/statistics.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/statistics_registry.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/statistics_registry.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/string.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/string.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/tuple.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/unsafe_interrupt_exception.h
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/utility.cpp
/usr/src/debug/cvc4-1.8-13.fc37.x86_64/src/util/utility.h

Generated by rpm2html 1.8.1

Fabrice Bellet, Tue Apr 9 18:50:33 2024