diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-09-05 14:00:52 -0700 |
|---|---|---|
| committer | Mathias Preiner <mathias.preiner@gmail.com> | 2018-09-22 16:30:59 -0700 |
| commit | 2e931a009cc474a6c326fc9a1b1b289198a50838 (patch) | |
| tree | 3543ef7c88856a19ff96e30c02b69393469d8930 | |
| parent | 32bc6b382859a96f08f7ef78c0d64efc5235d227 (diff) | |
cmake: Rebase with current master, add new tests/source files.
| -rw-r--r-- | doc/CMakeLists.txt | 4 | ||||
| -rw-r--r-- | src/CMakeLists.txt | 77 | ||||
| -rw-r--r-- | src/bindings/compat/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/bindings/compat/c/CMakeLists.txt | 0 | ||||
| -rw-r--r-- | src/bindings/compat/java/CMakeLists.txt | 0 | ||||
| -rw-r--r-- | src/compat/CMakeLists.txt | 8 | ||||
| -rw-r--r-- | src/expr/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/util/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 3975 | ||||
| -rw-r--r-- | test/system/CMakeLists.txt | 4 |
10 files changed, 2079 insertions, 1995 deletions
diff --git a/doc/CMakeLists.txt b/doc/CMakeLists.txt index bbde816e4..52867433e 100644 --- a/doc/CMakeLists.txt +++ b/doc/CMakeLists.txt @@ -15,10 +15,6 @@ configure_file( ${CMAKE_CURRENT_BINARY_DIR}/libcvc4.3) configure_file( - ${CMAKE_CURRENT_SOURCE_DIR}/libcvc4compat.3.in - ${CMAKE_CURRENT_BINARY_DIR}/libcvc4compat.3) - -configure_file( ${CMAKE_CURRENT_SOURCE_DIR}/libcvc4parser.3.in ${CMAKE_CURRENT_BINARY_DIR}/libcvc4parser.3) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 22513d47e..8e8e0bd45 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -26,44 +26,78 @@ set(cvc4_src_files decision/decision_strategy.h decision/justification_heuristic.cpp decision/justification_heuristic.h + preprocessing/assertion_pipeline.cpp + preprocessing/assertion_pipeline.h preprocessing/passes/apply_substs.cpp preprocessing/passes/apply_substs.h + preprocessing/passes/apply_to_const.cpp + preprocessing/passes/apply_to_const.h preprocessing/passes/bool_to_bv.cpp preprocessing/passes/bool_to_bv.h preprocessing/passes/bv_abstraction.cpp preprocessing/passes/bv_abstraction.h preprocessing/passes/bv_ackermann.cpp preprocessing/passes/bv_ackermann.h + preprocessing/passes/bv_eager_atoms.cpp + preprocessing/passes/bv_eager_atoms.h preprocessing/passes/bv_gauss.cpp preprocessing/passes/bv_gauss.h preprocessing/passes/bv_intro_pow2.cpp preprocessing/passes/bv_intro_pow2.h preprocessing/passes/bv_to_bool.cpp preprocessing/passes/bv_to_bool.h + preprocessing/passes/extended_rewriter_pass.cpp + preprocessing/passes/extended_rewriter_pass.h + preprocessing/passes/global_negate.cpp + preprocessing/passes/global_negate.h preprocessing/passes/int_to_bv.cpp preprocessing/passes/int_to_bv.h + preprocessing/passes/ite_removal.cpp + preprocessing/passes/ite_removal.h + preprocessing/passes/ite_simp.cpp + preprocessing/passes/ite_simp.h + preprocessing/passes/miplib_trick.cpp + preprocessing/passes/miplib_trick.h + preprocessing/passes/nl_ext_purify.cpp + preprocessing/passes/nl_ext_purify.h + preprocessing/passes/non_clausal_simp.cpp + preprocessing/passes/non_clausal_simp.h preprocessing/passes/pseudo_boolean_processor.cpp preprocessing/passes/pseudo_boolean_processor.h + preprocessing/passes/quantifier_macros.cpp + preprocessing/passes/quantifier_macros.h + preprocessing/passes/quantifiers_preprocess.cpp + preprocessing/passes/quantifiers_preprocess.h preprocessing/passes/real_to_int.cpp preprocessing/passes/real_to_int.h preprocessing/passes/rewrite.cpp preprocessing/passes/rewrite.h preprocessing/passes/sep_skolem_emp.cpp preprocessing/passes/sep_skolem_emp.h + preprocessing/passes/sort_infer.cpp + preprocessing/passes/sort_infer.h preprocessing/passes/static_learning.cpp preprocessing/passes/static_learning.h + preprocessing/passes/sygus_inference.cpp + preprocessing/passes/sygus_inference.h preprocessing/passes/symmetry_breaker.cpp preprocessing/passes/symmetry_breaker.h preprocessing/passes/symmetry_detect.cpp preprocessing/passes/symmetry_detect.h preprocessing/passes/synth_rew_rules.cpp preprocessing/passes/synth_rew_rules.h + preprocessing/passes/theory_preprocess.cpp + preprocessing/passes/theory_preprocess.h + preprocessing/passes/unconstrained_simplifier.cpp + preprocessing/passes/unconstrained_simplifier.h preprocessing/preprocessing_pass.cpp preprocessing/preprocessing_pass.h preprocessing/preprocessing_pass_context.cpp preprocessing/preprocessing_pass_context.h preprocessing/preprocessing_pass_registry.cpp preprocessing/preprocessing_pass_registry.h + preprocessing/util/ite_utilities.cpp + preprocessing/util/ite_utilities.h printer/ast/ast_printer.cpp printer/ast/ast_printer.h printer/cvc/cvc_printer.cpp @@ -89,6 +123,8 @@ set(cvc4_src_files proof/cnf_proof.h proof/lemma_proof.cpp proof/lemma_proof.h + proof/lfsc_proof_printer.cpp + proof/lfsc_proof_printer.h proof/proof.h proof/proof_manager.cpp proof/proof_manager.h @@ -136,6 +172,8 @@ set(cvc4_src_files smt/managed_ostreams.h smt/model.cpp smt/model.h + smt/model_core_builder.cpp + smt/model_core_builder.h smt/smt_engine.cpp smt/smt_engine.h smt/smt_engine_check_proof.cpp @@ -297,6 +335,10 @@ set(cvc4_src_files theory/datatypes/theory_datatypes_type_rules.h theory/datatypes/type_enumerator.cpp theory/datatypes/type_enumerator.h + theory/decision_manager.cpp + theory/decision_manager.h + theory/decision_strategy.cpp + theory/decision_strategy.h theory/evaluator.cpp theory/evaluator.h theory/ext_theory.cpp @@ -318,8 +360,6 @@ set(cvc4_src_files theory/idl/theory_idl.cpp theory/idl/theory_idl.h theory/interrupted.h - theory/ite_utilities.cpp - theory/ite_utilities.h theory/logic_info.cpp theory/logic_info.h theory/output_channel.h @@ -343,8 +383,8 @@ set(cvc4_src_files theory/quantifiers/cegqi/ceg_epr_instantiator.h theory/quantifiers/cegqi/ceg_instantiator.cpp theory/quantifiers/cegqi/ceg_instantiator.h - theory/quantifiers/cegqi/inst_strategy_cbqi.cpp - theory/quantifiers/cegqi/inst_strategy_cbqi.h + theory/quantifiers/cegqi/inst_strategy_cegqi.cpp + theory/quantifiers/cegqi/inst_strategy_cegqi.h theory/quantifiers/conjecture_generator.cpp theory/quantifiers/conjecture_generator.h theory/quantifiers/dynamic_rewrite.cpp @@ -365,6 +405,10 @@ set(cvc4_src_files theory/quantifiers/equality_infer.h theory/quantifiers/equality_query.cpp theory/quantifiers/equality_query.h + theory/quantifiers/expr_miner.cpp + theory/quantifiers/expr_miner.h + theory/quantifiers/expr_miner_manager.cpp + theory/quantifiers/expr_miner_manager.h theory/quantifiers/extended_rewrite.cpp theory/quantifiers/extended_rewrite.h theory/quantifiers/first_order_model.cpp @@ -381,8 +425,6 @@ set(cvc4_src_files theory/quantifiers/fmf/model_engine.h theory/quantifiers/fun_def_process.cpp theory/quantifiers/fun_def_process.h - theory/quantifiers/global_negate.cpp - theory/quantifiers/global_negate.h theory/quantifiers/inst_match.cpp theory/quantifiers/inst_match.h theory/quantifiers/inst_match_trie.cpp @@ -397,8 +439,6 @@ set(cvc4_src_files theory/quantifiers/lazy_trie.h theory/quantifiers/local_theory_ext.cpp theory/quantifiers/local_theory_ext.h - theory/quantifiers/macros.cpp - theory/quantifiers/macros.h theory/quantifiers/quant_conflict_find.cpp theory/quantifiers/quant_conflict_find.h theory/quantifiers/quant_epr.cpp @@ -421,10 +461,6 @@ set(cvc4_src_files theory/quantifiers/single_inv_partition.h theory/quantifiers/skolemize.cpp theory/quantifiers/skolemize.h - theory/quantifiers/sygus/ce_guided_conjecture.cpp - theory/quantifiers/sygus/ce_guided_conjecture.h - theory/quantifiers/sygus/ce_guided_instantiation.cpp - theory/quantifiers/sygus/ce_guided_instantiation.h theory/quantifiers/sygus/ce_guided_single_inv.cpp theory/quantifiers/sygus/ce_guided_single_inv.h theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -461,12 +497,16 @@ set(cvc4_src_files theory/quantifiers/sygus/sygus_unif_rl.h theory/quantifiers/sygus/sygus_unif_strat.cpp theory/quantifiers/sygus/sygus_unif_strat.h + theory/quantifiers/sygus/synth_conjecture.cpp + theory/quantifiers/sygus/synth_conjecture.h + theory/quantifiers/sygus/synth_engine.cpp + theory/quantifiers/sygus/synth_engine.h theory/quantifiers/sygus/term_database_sygus.cpp theory/quantifiers/sygus/term_database_sygus.h - theory/quantifiers/sygus_inference.cpp - theory/quantifiers/sygus_inference.h theory/quantifiers/sygus_sampler.cpp theory/quantifiers/sygus_sampler.h + theory/quantifiers/term_canonize.cpp + theory/quantifiers/term_canonize.h theory/quantifiers/term_database.cpp theory/quantifiers/term_database.h theory/quantifiers/term_enumeration.cpp @@ -504,8 +544,12 @@ set(cvc4_src_files theory/shared_terms_database.h theory/sort_inference.cpp theory/sort_inference.h + theory/strings/regexp_elim.cpp + theory/strings/regexp_elim.h theory/strings/regexp_operation.cpp theory/strings/regexp_operation.h + theory/strings/skolem_cache.cpp + theory/strings/skolem_cache.h theory/strings/theory_strings.cpp theory/strings/theory_strings.h theory/strings/theory_strings_preprocess.cpp @@ -514,6 +558,8 @@ set(cvc4_src_files theory/strings/theory_strings_rewriter.h theory/strings/theory_strings_type_rules.h theory/strings/type_enumerator.h + theory/subs_minimize.cpp + theory/subs_minimize.h theory/substitutions.cpp theory/substitutions.h theory/term_registration_visitor.cpp @@ -544,8 +590,6 @@ set(cvc4_src_files theory/uf/theory_uf_strong_solver.cpp theory/uf/theory_uf_strong_solver.h theory/uf/theory_uf_type_rules.h - theory/unconstrained_simplifier.cpp - theory/unconstrained_simplifier.h theory/valuation.cpp theory/valuation.h ) @@ -578,7 +622,6 @@ include_directories(include) include_directories(. ${CMAKE_CURRENT_BINARY_DIR}) add_subdirectory(base) -add_subdirectory(compat) add_subdirectory(expr) add_subdirectory(lib) add_subdirectory(main) diff --git a/src/bindings/compat/CMakeLists.txt b/src/bindings/compat/CMakeLists.txt deleted file mode 100644 index 92c37023a..000000000 --- a/src/bindings/compat/CMakeLists.txt +++ /dev/null @@ -1,2 +0,0 @@ -add_subdirectory(c) -add_subdirectory(java) diff --git a/src/bindings/compat/c/CMakeLists.txt b/src/bindings/compat/c/CMakeLists.txt deleted file mode 100644 index e69de29bb..000000000 --- a/src/bindings/compat/c/CMakeLists.txt +++ /dev/null diff --git a/src/bindings/compat/java/CMakeLists.txt b/src/bindings/compat/java/CMakeLists.txt deleted file mode 100644 index e69de29bb..000000000 --- a/src/bindings/compat/java/CMakeLists.txt +++ /dev/null diff --git a/src/compat/CMakeLists.txt b/src/compat/CMakeLists.txt deleted file mode 100644 index f327de593..000000000 --- a/src/compat/CMakeLists.txt +++ /dev/null @@ -1,8 +0,0 @@ -set(compat_src_files - cvc3_compat.cpp - cvc3_compat.h -) - -add_library(cvc4compat ${compat_src_files}) -target_compile_definitions(cvc4compat PRIVATE -D__BUILDING_CVC4COMPATLIB) -target_link_libraries(cvc4compat cvc4) diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 0421261a2..c11333bff 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -18,6 +18,8 @@ set(expr_src_files matcher.h node.cpp node.h + node_algorithm.cpp + node_algorithm.h node_builder.h node_manager.cpp node_manager.h diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 724a1ae5a..de748ad98 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -16,14 +16,12 @@ set(util_src_files dense_map.h divisible.cpp divisible.h - dynamic_array.h floatingpoint.cpp gmp_util.h hash.h index.cpp index.h maybe.h - ntuple.h ostream_util.cpp ostream_util.h proof.h diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 32194dbee..c4ba87489 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1,1998 +1,2053 @@ set(regress_0_tests - regress0/arith/arith.01.cvc - regress0/arith/arith.02.cvc - regress0/arith/arith.03.cvc - regress0/arith/bug443.delta01.smt - regress0/arith/bug547.2.smt2 - regress0/arith/bug569.smt2 - regress0/arith/delta-minimized-row-vector-bug.smt - regress0/arith/div.01.smt2 - regress0/arith/div.02.smt2 - regress0/arith/div.04.smt2 - regress0/arith/div.05.smt2 - regress0/arith/div.07.smt2 - regress0/arith/fuzz_3-eq.smt - regress0/arith/integers/arith-int-042.cvc - regress0/arith/integers/arith-int-042.min.cvc - regress0/arith/leq.01.smt - regress0/arith/miplib.cvc - regress0/arith/miplib2.cvc - regress0/arith/miplib4.cvc - regress0/arith/miplibtrick.smt - regress0/arith/mod-simp.smt2 - regress0/arith/mod.01.smt2 - regress0/arith/mult.01.smt2 - regress0/arrayinuf_declare.smt2 - regress0/arrays/arrays0.smt2 - regress0/arrays/arrays1.smt2 - regress0/arrays/arrays2.smt2 - regress0/arrays/arrays3.smt2 - regress0/arrays/arrays4.smt2 - regress0/arrays/bool-array.smt2 - regress0/arrays/bug272.minimized.smt - regress0/arrays/bug272.smt - regress0/arrays/bug637.delta.smt2 - regress0/arrays/constarr.cvc - regress0/arrays/constarr.smt2 - regress0/arrays/constarr2.cvc - regress0/arrays/constarr2.smt2 - regress0/arrays/incorrect1.smt - regress0/arrays/incorrect10.smt - regress0/arrays/incorrect11.smt - regress0/arrays/incorrect2.minimized.smt - regress0/arrays/incorrect2.smt - regress0/arrays/incorrect3.smt - regress0/arrays/incorrect4.smt - regress0/arrays/incorrect5.smt - regress0/arrays/incorrect6.smt - regress0/arrays/incorrect7.smt - regress0/arrays/incorrect8.minimized.smt - regress0/arrays/incorrect8.smt - regress0/arrays/incorrect9.smt - regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smt - regress0/arrays/x2.smt - regress0/arrays/x3.smt - regress0/aufbv/array_rewrite_bug.smt - regress0/aufbv/bug00.smt - regress0/aufbv/bug338.smt2 - regress0/aufbv/bug347.smt - regress0/aufbv/bug451.smt - regress0/aufbv/bug509.smt - regress0/aufbv/bug580.delta.smt2 - regress0/aufbv/diseqprop.01.smt - regress0/aufbv/dubreva005ue.delta01.smt - regress0/aufbv/fifo32bc06k08.delta01.smt - regress0/aufbv/fuzz00.smt - regress0/aufbv/fuzz01.delta01.smt - regress0/aufbv/fuzz01.smt - regress0/aufbv/fuzz02.delta01.smt - regress0/aufbv/fuzz02.smt - regress0/aufbv/fuzz03.delta01.smt - regress0/aufbv/fuzz03.smt - regress0/aufbv/fuzz04.delta01.smt - regress0/aufbv/fuzz04.smt - regress0/aufbv/fuzz05.delta01.smt - regress0/aufbv/fuzz05.smt - regress0/aufbv/fuzz06.delta01.smt - regress0/aufbv/fuzz06.smt - regress0/aufbv/fuzz07.smt - regress0/aufbv/fuzz08.smt - regress0/aufbv/fuzz09.smt - regress0/aufbv/fuzz11.smt - regress0/aufbv/fuzz12.smt - regress0/aufbv/fuzz13.smt - regress0/aufbv/fuzz14.smt - regress0/aufbv/fuzz15.smt - regress0/aufbv/rewrite_bug.smt - regress0/aufbv/try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.delta01.smt - regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt - regress0/aufbv/wchains010ue.delta01.smt - regress0/aufbv/wchains010ue.delta02.smt - regress0/auflia/a17.smt - regress0/auflia/bug336.smt2 - regress0/auflia/error72.delta2.smt - regress0/auflia/fuzz-error1099.smt - regress0/auflia/fuzz-error232.smt - regress0/auflia/fuzz01.delta01.smt - regress0/auflia/fuzz02.smt - regress0/auflia/fuzz03.smt - regress0/auflia/fuzz04.smt - regress0/auflia/fuzz05.smt - regress0/auflia/x2.smt - regress0/boolean-prec.cvc - regress0/boolean-terms-bug-array.smt2 - regress0/boolean-terms-kernel1.smt2 - regress0/boolean-terms.cvc - regress0/bt-test-00.smt2 - regress0/bt-test-01.smt2 - regress0/bug1247.smt2 - regress0/bug161.smt - regress0/bug164.smt - regress0/bug167.smt - regress0/bug168.smt - regress0/bug187.smt2 - regress0/bug217.smt2 - regress0/bug220.smt2 - regress0/bug239.smt - regress0/bug274.cvc - regress0/bug288.smt - regress0/bug288b.smt - regress0/bug288c.smt - regress0/bug303.smt2 - regress0/bug310.cvc - regress0/bug32.cvc - regress0/bug322.cvc - regress0/bug322b.cvc - regress0/bug339.smt2 - regress0/bug365.smt2 - regress0/bug382.smt2 - regress0/bug383.smt2 - regress0/bug398.smt2 - regress0/bug421.smt2 - regress0/bug421b.smt2 - regress0/bug480.smt2 - regress0/bug484.smt2 - regress0/bug486.cvc - regress0/bug49.smt - regress0/bug512.minimized.smt2 - regress0/bug521.minimized.smt2 - regress0/bug522.smt2 - regress0/bug528a.smt2 - regress0/bug541.smt2 - regress0/bug544.smt2 - regress0/bug548a.smt2 - regress0/bug576.smt2 - regress0/bug576a.smt2 - regress0/bug578.smt2 - regress0/bug586.cvc - regress0/bug595.cvc - regress0/bug596.cvc - regress0/bug596b.cvc - regress0/bug605.cvc - regress0/bug639.smt2 - regress0/buggy-ite.smt2 - regress0/bv/bool-to-bv.smt2 - regress0/bv/bug260a.smt - regress0/bv/bug260b.smt - regress0/bv/bug440.smt - regress0/bv/bug733.smt2 - regress0/bv/bug734.smt2 - regress0/bv/bv-abstr-bug.smt2 - regress0/bv/bv-abstr-bug2.smt2 - regress0/bv/bv-int-collapse1.smt2 - regress0/bv/bv-int-collapse2.smt2 - regress0/bv/bv-options1.smt2 - regress0/bv/bv-options2.smt2 - regress0/bv/bv-options3.smt2 - regress0/bv/bv-options4.smt2 - regress0/bv/bv-to-bool.smt - regress0/bv/bv2nat-ground-c.smt2 - regress0/bv/bv2nat-simp-range.smt2 - regress0/bv/bvmul-pow2-only.smt2 - regress0/bv/bvsimple.cvc - regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt - regress0/bv/core/a78test0002.smt - regress0/bv/core/a95test0002.smt - regress0/bv/core/bitvec0.smt - regress0/bv/core/bitvec2.smt - regress0/bv/core/bitvec5.smt - regress0/bv/core/bitvec7.smt - regress0/bv/core/bv_eq_diamond10.smt - regress0/bv/core/concat-merge-0.smt - regress0/bv/core/concat-merge-1.smt - regress0/bv/core/concat-merge-2.smt - regress0/bv/core/concat-merge-3.smt - regress0/bv/core/equality-00.smt - regress0/bv/core/equality-01.smt - regress0/bv/core/equality-02.smt - regress0/bv/core/equality-05.smt - regress0/bv/core/extract-concat-0.smt - regress0/bv/core/extract-concat-1.smt - regress0/bv/core/extract-concat-10.smt - regress0/bv/core/extract-concat-11.smt - regress0/bv/core/extract-concat-2.smt - regress0/bv/core/extract-concat-3.smt - regress0/bv/core/extract-concat-4.smt - regress0/bv/core/extract-concat-5.smt - regress0/bv/core/extract-concat-6.smt - regress0/bv/core/extract-concat-7.smt - regress0/bv/core/extract-concat-8.smt - regress0/bv/core/extract-concat-9.smt - regress0/bv/core/extract-constant.smt - regress0/bv/core/extract-extract-0.smt - regress0/bv/core/extract-extract-1.smt - regress0/bv/core/extract-extract-10.smt - regress0/bv/core/extract-extract-11.smt - regress0/bv/core/extract-extract-2.smt - regress0/bv/core/extract-extract-3.smt - regress0/bv/core/extract-extract-4.smt - regress0/bv/core/extract-extract-5.smt - regress0/bv/core/extract-extract-6.smt - regress0/bv/core/extract-extract-7.smt - regress0/bv/core/extract-extract-8.smt - regress0/bv/core/extract-extract-9.smt - regress0/bv/core/extract-whole-0.smt - regress0/bv/core/extract-whole-1.smt - regress0/bv/core/extract-whole-2.smt - regress0/bv/core/extract-whole-3.smt - regress0/bv/core/extract-whole-4.smt - regress0/bv/core/slice-01.smt - regress0/bv/core/slice-02.smt - regress0/bv/core/slice-03.smt - regress0/bv/core/slice-04.smt - regress0/bv/core/slice-05.smt - regress0/bv/core/slice-06.smt - regress0/bv/core/slice-07.smt - regress0/bv/core/slice-08.smt - regress0/bv/core/slice-09.smt - regress0/bv/core/slice-10.smt - regress0/bv/core/slice-11.smt - regress0/bv/core/slice-12.smt - regress0/bv/core/slice-13.smt - regress0/bv/core/slice-14.smt - regress0/bv/core/slice-15.smt - regress0/bv/core/slice-16.smt - regress0/bv/core/slice-17.smt - regress0/bv/core/slice-18.smt - regress0/bv/core/slice-19.smt - regress0/bv/core/slice-20.smt - regress0/bv/eager-inc-cryptominisat.smt2 - regress0/bv/divtest_2_5.smt2 - regress0/bv/divtest_2_6.smt2 - regress0/bv/fuzz01.smt - regress0/bv/fuzz02.delta01.smt - regress0/bv/fuzz02.smt - regress0/bv/fuzz03.smt - regress0/bv/fuzz04.smt - regress0/bv/fuzz05.smt - regress0/bv/fuzz06.smt - regress0/bv/fuzz07.smt - regress0/bv/fuzz08.smt - regress0/bv/fuzz09.smt - regress0/bv/fuzz10.smt - regress0/bv/fuzz11.smt - regress0/bv/fuzz12.smt - regress0/bv/fuzz13.smt - regress0/bv/fuzz14.smt - regress0/bv/fuzz16.delta01.smt - regress0/bv/fuzz17.delta01.smt - regress0/bv/fuzz18.delta01.smt - regress0/bv/fuzz18.delta02.smt - regress0/bv/fuzz18.delta03.smt - regress0/bv/fuzz18.smt - regress0/bv/fuzz19.delta01.smt - regress0/bv/fuzz19.smt - regress0/bv/fuzz20.delta01.smt - regress0/bv/fuzz20.smt - regress0/bv/fuzz21.delta01.smt - regress0/bv/fuzz21.smt - regress0/bv/fuzz22.delta01.smt - regress0/bv/fuzz22.smt - regress0/bv/fuzz23.delta01.smt - regress0/bv/fuzz23.smt - regress0/bv/fuzz24.delta01.smt - regress0/bv/fuzz24.smt - regress0/bv/fuzz25.delta01.smt - regress0/bv/fuzz25.smt - regress0/bv/fuzz26.delta01.smt - regress0/bv/fuzz26.smt - regress0/bv/fuzz27.delta01.smt - regress0/bv/fuzz27.smt - regress0/bv/fuzz28.delta01.smt - regress0/bv/fuzz28.smt - regress0/bv/fuzz29.delta01.smt - regress0/bv/fuzz29.smt - regress0/bv/fuzz30.delta01.smt - regress0/bv/fuzz30.smt - regress0/bv/fuzz31.delta01.smt - regress0/bv/fuzz31.smt - regress0/bv/fuzz32.delta01.smt - regress0/bv/fuzz32.smt - regress0/bv/fuzz33.delta01.smt - regress0/bv/fuzz33.smt - regress0/bv/fuzz34.delta01.smt - regress0/bv/fuzz35.delta01.smt - regress0/bv/fuzz35.smt - regress0/bv/fuzz36.delta01.smt - regress0/bv/fuzz36.smt - regress0/bv/fuzz37.delta01.smt - regress0/bv/fuzz37.smt - regress0/bv/fuzz38.delta01.smt - regress0/bv/fuzz39.delta01.smt - regress0/bv/fuzz39.smt - regress0/bv/fuzz40.delta01.smt - regress0/bv/fuzz40.smt - regress0/bv/fuzz41.smt - regress0/bv/mul-neg-unsat.smt2 - regress0/bv/mul-negpow2.smt2 - regress0/bv/mult-pow2-negative.smt2 - regress0/bv/sizecheck.cvc - regress0/bv/smtcompbug.smt - regress0/bv/test-bv_intro_pow2.smt2 - regress0/bv/unsound1-reduced.smt2 - regress0/chained-equality.smt2 - regress0/constant-rewrite.smt - regress0/cvc3.userdoc.01.cvc - regress0/cvc3.userdoc.02.cvc - regress0/cvc3.userdoc.03.cvc - regress0/cvc3.userdoc.04.cvc - regress0/cvc3.userdoc.05.cvc - regress0/cvc3.userdoc.06.cvc - regress0/datatypes/Test1-tup-mp.cvc - regress0/datatypes/boolean-equality.cvc - regress0/datatypes/boolean-terms-datatype.cvc - regress0/datatypes/boolean-terms-parametric-datatype-1.cvc - regress0/datatypes/boolean-terms-parametric-datatype-2.cvc - regress0/datatypes/boolean-terms-record.cvc - regress0/datatypes/boolean-terms-rewrite.cvc - regress0/datatypes/boolean-terms-tuple.cvc - regress0/datatypes/bug286.cvc - regress0/datatypes/bug438.cvc - regress0/datatypes/bug438b.cvc - regress0/datatypes/bug597-rbt.smt2 - regress0/datatypes/bug604.smt2 - regress0/datatypes/bug625.smt2 - regress0/datatypes/cdt-model-cade15.smt2 - regress0/datatypes/cdt-non-canon-stream.smt2 - regress0/datatypes/coda_simp_model.smt2 - regress0/datatypes/conqueue-dt-enum-iloop.smt2 - regress0/datatypes/datatype.cvc - regress0/datatypes/datatype0.cvc - regress0/datatypes/datatype1.cvc - regress0/datatypes/datatype13.cvc - regress0/datatypes/datatype2.cvc - regress0/datatypes/datatype3.cvc - regress0/datatypes/datatype4.cvc - regress0/datatypes/dt-2.6.smt2 - regress0/datatypes/dt-match-pat-param-2.6.smt2 - regress0/datatypes/dt-param-2.6.smt2 - regress0/datatypes/dt-param-card4-bool-sat.smt2 - regress0/datatypes/dt-sel-2.6.smt2 - regress0/datatypes/empty_tuprec.cvc - regress0/datatypes/example-dailler-min.smt2 - regress0/datatypes/is_test.smt2 - regress0/datatypes/issue1433.smt2 - regress0/datatypes/jsat-2.6.smt2 - regress0/datatypes/model-subterms-min.smt2 - regress0/datatypes/mutually-recursive.cvc - regress0/datatypes/pair-bool-bool.cvc - regress0/datatypes/pair-real-bool.smt2 - regress0/datatypes/rec1.cvc - regress0/datatypes/rec2.cvc - regress0/datatypes/rec4.cvc - regress0/datatypes/rewriter.cvc - regress0/datatypes/sc-cdt1.smt2 - regress0/datatypes/some-boolean-tests.cvc - regress0/datatypes/stream-singleton.smt2 - regress0/datatypes/tenum-bug.smt2 - regress0/datatypes/tuple-model.cvc - regress0/datatypes/tuple-no-clash.cvc - regress0/datatypes/tuple-record-bug.cvc - regress0/datatypes/tuple.cvc - regress0/datatypes/tuples-empty.smt2 - regress0/datatypes/tuples-multitype.smt2 - regress0/datatypes/typed_v10l30054.cvc - regress0/datatypes/typed_v1l80005.cvc - regress0/datatypes/typed_v2l30079.cvc - regress0/datatypes/typed_v3l20092.cvc - regress0/datatypes/typed_v5l30069.cvc - regress0/datatypes/v10l40099.cvc - regress0/datatypes/v2l40025.cvc - regress0/datatypes/v3l60006.cvc - regress0/datatypes/v5l30058.cvc - regress0/datatypes/wrong-sel-simp.cvc - regress0/decision/aufbv-fuzz01.smt - regress0/decision/bitvec0.delta01.smt - regress0/decision/bitvec0.smt - regress0/decision/bitvec5.smt - regress0/decision/bug347.smt - regress0/decision/bug374a.smt - regress0/decision/bug374b.smt2 - regress0/decision/error122.delta01.smt - regress0/decision/error122.smt - regress0/decision/error20.delta01.smt - regress0/decision/error20.smt - regress0/decision/error3.delta01.smt - regress0/decision/pp-regfile.delta01.smt - regress0/decision/pp-regfile.delta02.smt - regress0/decision/quant-ex1.smt2 - regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt - regress0/decision/wchains010ue.delta02.smt - regress0/declare-fun-is-match.smt2 - regress0/declare-funs.smt2 - regress0/distinct.smt - regress0/expect/scrub.01.smt - regress0/expect/scrub.02.smt - regress0/expect/scrub.03.smt2 - regress0/expect/scrub.04.smt2 - regress0/expect/scrub.06.cvc - regress0/expect/scrub.08.sy - regress0/expect/scrub.09.p - regress0/flet.smt - regress0/flet2.smt - regress0/fmf/Arrow_Order-smtlib.778341.smt - regress0/fmf/QEpres-uf.855035.smt - regress0/fmf/array_card.smt2 - regress0/fmf/bounded_sets.smt2 - regress0/fmf/bug-041417-set-options.cvc - regress0/fmf/bug652.smt2 - regress0/fmf/bug782.smt2 - regress0/fmf/cruanes-no-minimal-unk.smt2 - regress0/fmf/fc-simple.smt2 - regress0/fmf/fc-unsat-pent.smt2 - regress0/fmf/fc-unsat-tot-2.smt2 - regress0/fmf/fd-false.smt2 - regress0/fmf/fmc_unsound_model.smt2 - regress0/fmf/fmf-strange-bounds-2.smt2 - regress0/fmf/forall_unit_data2.smt2 - regress0/fmf/krs-sat.smt2 - regress0/fmf/no-minimal-sat.smt2 - regress0/fmf/quant_real_univ.cvc - regress0/fmf/sat-logic.smt2 - regress0/fmf/sc_bad_model_1221.smt2 - regress0/fmf/syn002-si-real-int.smt2 - regress0/fmf/tail_rec.smt2 - regress0/fp/simple.smt2 - regress0/fuzz_1.smt - regress0/fuzz_3.smt - regress0/get-value-incremental.smt2 - regress0/get-value-ints.smt2 - regress0/get-value-reals-ints.smt2 - regress0/get-value-reals.smt2 - regress0/ho/apply-collapse-sat.smt2 - regress0/ho/apply-collapse-unsat.smt2 - regress0/ho/cong-full-apply.smt2 - regress0/ho/cong.smt2 - regress0/ho/declare-fun-variants.smt2 - regress0/ho/def-fun-flatten.smt2 - regress0/ho/ext-finite-unsat.smt2 - regress0/ho/ext-ho-nested-lambda-model.smt2 - regress0/ho/ext-ho.smt2 - regress0/ho/ext-sat-partial-eval.smt2 - regress0/ho/ext-sat.smt2 - regress0/ho/finite-fun-ext.smt2 - regress0/ho/fta0144-alpha-eq.smt2 - regress0/ho/ho-match-fun-suffix.smt2 - regress0/ho/ho-matching-enum.smt2 - regress0/ho/ho-matching-nested-app.smt2 - regress0/ho/ite-apply-eq.smt2 - regress0/ho/lambda-equality-non-canon.smt2 - regress0/ho/modulo-func-equality.smt2 - regress0/ho/simple-matching-partial.smt2 - regress0/ho/simple-matching.smt2 - regress0/ho/trans.smt2 - regress0/hung10_itesdk_output1.smt2 - regress0/hung10_itesdk_output2.smt2 - regress0/hung13sdk_output1.smt2 - regress0/hung13sdk_output2.smt2 - regress0/ineq_basic.smt - regress0/ineq_slack.smt - regress0/issue1063-overloading-dt-cons.smt2 - regress0/issue1063-overloading-dt-fun.smt2 - regress0/issue1063-overloading-dt-sel.smt2 - regress0/ite.cvc - regress0/ite2.smt2 - regress0/ite3.smt2 - regress0/ite4.smt2 - regress0/ite_real_int_type.smt - regress0/ite_real_valid.smt - regress0/lang_opts_2_5.smt2 - regress0/lang_opts_2_6_1.smt2 - regress0/lemmas/clocksynchro_5clocks.main_invar.base.model.smt - regress0/lemmas/fs_not_sc_seen.induction.smt - regress0/lemmas/mode_cntrl.induction.smt - regress0/lemmas/sc_init_frame_gap.induction.smt - regress0/let.cvc - regress0/let.smt - regress0/let2.smt - regress0/logops.01.cvc - regress0/logops.02.cvc - regress0/logops.03.cvc - regress0/logops.04.cvc - regress0/logops.05.cvc - regress0/nl/coeff-sat.smt2 - regress0/nl/magnitude-wrong-1020-m.smt2 - regress0/nl/mult-po.smt2 - regress0/nl/nia-wrong-tl.smt2 - regress0/nl/nta/cos-sig-value.smt2 - regress0/nl/nta/exp-n0.5-lb.smt2 - regress0/nl/nta/exp-n0.5-ub.smt2 - regress0/nl/nta/exp1-ub.smt2 - regress0/nl/nta/real-pi.smt2 - regress0/nl/nta/sin-sym.smt2 - regress0/nl/nta/sqrt-simple.smt2 - regress0/nl/nta/tan-rewrite.smt2 - regress0/nl/real-as-int.smt2 - regress0/nl/real-div-ufnra.smt2 - regress0/nl/subs0-unsat-confirm.smt2 - regress0/nl/very-easy-sat.smt2 - regress0/nl/very-simple-unsat.smt2 - regress0/parallel-let.smt2 - regress0/parser/as.smt2 - regress0/parser/constraint.smt2 - regress0/parser/declarefun-emptyset-uf.smt2 - regress0/parser/shadow_fun_symbol_all.smt2 - regress0/parser/shadow_fun_symbol_nirat.smt2 - regress0/parser/strings20.smt2 - regress0/parser/strings25.smt2 - regress0/precedence/and-not.cvc - regress0/precedence/and-xor.cvc - regress0/precedence/bool-cmp.cvc - regress0/precedence/cmp-plus.cvc - regress0/precedence/eq-fun.cvc - regress0/precedence/iff-assoc.cvc - regress0/precedence/iff-implies.cvc - regress0/precedence/implies-assoc.cvc - regress0/precedence/implies-iff.cvc - regress0/precedence/implies-or.cvc - regress0/precedence/not-and.cvc - regress0/precedence/not-eq.cvc - regress0/precedence/or-implies.cvc - regress0/precedence/or-xor.cvc - regress0/precedence/plus-mult.cvc - regress0/precedence/xor-and.cvc - regress0/precedence/xor-assoc.cvc - regress0/precedence/xor-or.cvc - regress0/preprocess/preprocess_00.cvc - regress0/preprocess/preprocess_01.cvc - regress0/preprocess/preprocess_02.cvc - regress0/preprocess/preprocess_03.cvc - regress0/preprocess/preprocess_04.cvc - regress0/preprocess/preprocess_05.cvc - regress0/preprocess/preprocess_06.cvc - regress0/preprocess/preprocess_07.cvc - regress0/preprocess/preprocess_08.cvc - regress0/preprocess/preprocess_09.cvc - regress0/preprocess/preprocess_10.cvc - regress0/preprocess/preprocess_11.cvc - regress0/preprocess/preprocess_12.cvc - regress0/preprocess/preprocess_13.cvc - regress0/preprocess/preprocess_14.cvc - regress0/preprocess/preprocess_15.cvc - regress0/print_lambda.cvc - regress0/push-pop/boolean/fuzz_12.smt2 - regress0/push-pop/boolean/fuzz_13.smt2 - regress0/push-pop/boolean/fuzz_14.smt2 - regress0/push-pop/boolean/fuzz_18.smt2 - regress0/push-pop/boolean/fuzz_2.smt2 - regress0/push-pop/boolean/fuzz_21.smt2 - regress0/push-pop/boolean/fuzz_22.smt2 - regress0/push-pop/boolean/fuzz_27.smt2 - regress0/push-pop/boolean/fuzz_3.smt2 - regress0/push-pop/boolean/fuzz_31.smt2 - regress0/push-pop/boolean/fuzz_33.smt2 - regress0/push-pop/boolean/fuzz_36.smt2 - regress0/push-pop/boolean/fuzz_38.smt2 - regress0/push-pop/boolean/fuzz_46.smt2 - regress0/push-pop/boolean/fuzz_47.smt2 - regress0/push-pop/boolean/fuzz_48.smt2 - regress0/push-pop/boolean/fuzz_49.smt2 - regress0/push-pop/boolean/fuzz_50.smt2 - regress0/push-pop/bug1990.smt2 - regress0/push-pop/bug233.cvc - regress0/push-pop/bug654-dd.smt2 - regress0/push-pop/bug691.smt2 - regress0/push-pop/bug821-check_sat_assuming.smt2 - regress0/push-pop/bug821.smt2 - regress0/push-pop/inc-define.smt2 - regress0/push-pop/inc-double-u.smt2 - regress0/push-pop/incremental-subst-bug.cvc - regress0/push-pop/issue1986.smt2 - regress0/push-pop/issue2137.min.smt2 - regress0/push-pop/quant-fun-proc-unfd.smt2 - regress0/push-pop/simple_unsat_cores.smt2 - regress0/push-pop/test.00.cvc - regress0/push-pop/test.01.cvc - regress0/push-pop/tiny_bug.smt2 - regress0/push-pop/units.cvc - regress0/quantifiers/ARI176e1.smt2 - regress0/quantifiers/agg-rew-test-cf.smt2 - regress0/quantifiers/agg-rew-test.smt2 - regress0/quantifiers/ari056.smt2 - regress0/quantifiers/bug269.smt2 - regress0/quantifiers/bug290.smt2 - regress0/quantifiers/bug291.smt2 - regress0/quantifiers/bug749-rounding.smt2 - regress0/quantifiers/cbqi-lia-dt-simp.smt2 - regress0/quantifiers/cegqi-nl-simp.cvc - regress0/quantifiers/cegqi-nl-sq.smt2 - regress0/quantifiers/clock-10.smt2 - regress0/quantifiers/clock-3.smt2 - regress0/quantifiers/delta-simp.smt2 - regress0/quantifiers/double-pattern.smt2 - regress0/quantifiers/ex3.smt2 - regress0/quantifiers/ex6.smt2 - regress0/quantifiers/floor.smt2 - regress0/quantifiers/horn-ground-pre-post.smt2 - regress0/quantifiers/is-even-pred.smt2 - regress0/quantifiers/is-int.smt2 - regress0/quantifiers/issue1805.smt2 - regress0/quantifiers/issue2031-bv-var-elim.smt2 - regress0/quantifiers/issue2033-macro-arith.smt2 - regress0/quantifiers/lra-triv-gn.smt2 - regress0/quantifiers/macros-int-real.smt2 - regress0/quantifiers/macros-real-arg.smt2 - regress0/quantifiers/matching-lia-1arg.smt2 - regress0/quantifiers/mix-complete-strat.smt2 - regress0/quantifiers/mix-match.smt2 - regress0/quantifiers/mix-simp.smt2 - regress0/quantifiers/nested-delta.smt2 - regress0/quantifiers/nested-inf.smt2 - regress0/quantifiers/partial-trigger.smt2 - regress0/quantifiers/pure_dt_cbqi.smt2 - regress0/quantifiers/qbv-inequality2.smt2 - regress0/quantifiers/qbv-simp.smt2 - regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 - regress0/quantifiers/qbv-test-invert-bvand-neq.smt2 - regress0/quantifiers/qbv-test-invert-bvand.smt2 - regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2 - regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2 - regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 - regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 - regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2 - regress0/quantifiers/qbv-test-invert-bvor-neq.smt2 - regress0/quantifiers/qbv-test-invert-bvor.smt2 - regress0/quantifiers/qbv-test-invert-bvshl-0.smt2 - regress0/quantifiers/qbv-test-invert-bvult-1.smt2 - regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2 - regress0/quantifiers/qbv-test-invert-bvxor.smt2 - regress0/quantifiers/qbv-test-invert-concat-0.smt2 - regress0/quantifiers/qbv-test-invert-concat-1.smt2 - regress0/quantifiers/qbv-test-invert-sign-extend.smt2 - regress0/quantifiers/qcf-rel-dom-opt.smt2 - regress0/quantifiers/rew-to-scala.smt2 - regress0/quantifiers/simp-len.smt2 - regress0/quantifiers/simp-typ-test.smt2 - regress0/queries0.cvc - regress0/rec-fun-const-parse-bug.smt2 - regress0/rels/addr_book_0.cvc - regress0/rels/atom_univ2.cvc - regress0/rels/card_transpose.cvc - regress0/rels/iden_0.cvc - regress0/rels/iden_1.cvc - regress0/rels/join-eq-u-sat.cvc - regress0/rels/join-eq-u.cvc - regress0/rels/joinImg_0.cvc - regress0/rels/oneLoc_no_quant-int_0_1.cvc - regress0/rels/rel_1tup_0.cvc - regress0/rels/rel_complex_0.cvc - regress0/rels/rel_complex_1.cvc - regress0/rels/rel_conflict_0.cvc - regress0/rels/rel_join_0.cvc - regress0/rels/rel_join_0_1.cvc - regress0/rels/rel_join_1.cvc - regress0/rels/rel_join_1_1.cvc - regress0/rels/rel_join_2.cvc - regress0/rels/rel_join_2_1.cvc - regress0/rels/rel_join_3.cvc - regress0/rels/rel_join_3_1.cvc - regress0/rels/rel_join_4.cvc - regress0/rels/rel_join_5.cvc - regress0/rels/rel_join_6.cvc - regress0/rels/rel_join_7.cvc - regress0/rels/rel_product_0.cvc - regress0/rels/rel_product_0_1.cvc - regress0/rels/rel_product_1.cvc - regress0/rels/rel_product_1_1.cvc - regress0/rels/rel_symbolic_1.cvc - regress0/rels/rel_symbolic_1_1.cvc - regress0/rels/rel_symbolic_2_1.cvc - regress0/rels/rel_symbolic_3_1.cvc - regress0/rels/rel_tc_11.cvc - regress0/rels/rel_tc_2_1.cvc - regress0/rels/rel_tc_3.cvc - regress0/rels/rel_tc_3_1.cvc - regress0/rels/rel_tc_7.cvc - regress0/rels/rel_tc_8.cvc - regress0/rels/rel_tp_3_1.cvc - regress0/rels/rel_tp_join_0.cvc - regress0/rels/rel_tp_join_1.cvc - regress0/rels/rel_tp_join_2.cvc - regress0/rels/rel_tp_join_3.cvc - regress0/rels/rel_tp_join_eq_0.cvc - regress0/rels/rel_tp_join_int_0.cvc - regress0/rels/rel_tp_join_pro_0.cvc - regress0/rels/rel_tp_join_var_0.cvc - regress0/rels/rel_transpose_0.cvc - regress0/rels/rel_transpose_1.cvc - regress0/rels/rel_transpose_1_1.cvc - regress0/rels/rel_transpose_3.cvc - regress0/rels/rel_transpose_4.cvc - regress0/rels/rel_transpose_5.cvc - regress0/rels/rel_transpose_6.cvc - regress0/rels/rel_transpose_7.cvc - regress0/rels/relations-ops.smt2 - regress0/rels/rels-sharing-simp.cvc - regress0/reset-assertions.smt2 - regress0/rewriterules/datatypes.smt2 - regress0/rewriterules/length_trick.smt2 - regress0/rewriterules/native_arrays.smt2 - regress0/rewriterules/relation.smt2 - regress0/rewriterules/simulate_rewriting.smt2 - regress0/sep/dispose-1.smt2 - regress0/sep/dup-nemp.smt2 - regress0/sep/nemp.smt2 - regress0/sep/nil-no-elim.smt2 - regress0/sep/nspatial-simp.smt2 - regress0/sep/pto-01.smt2 - regress0/sep/pto-02.smt2 - regress0/sep/sep-01.smt2 - regress0/sep/sep-plus1.smt2 - regress0/sep/sep-simp-unsat-emp.smt2 - regress0/sep/skolem_emp.smt2 - regress0/sep/trees-1.smt2 - regress0/sep/wand-crash.smt2 - regress0/sets/abt-min.smt2 - regress0/sets/abt-te-exh.smt2 - regress0/sets/abt-te-exh2.smt2 - regress0/sets/card-2.smt2 - regress0/sets/card-3sets.cvc - regress0/sets/card.smt2 - regress0/sets/card3-ground.smt2 - regress0/sets/complement.cvc - regress0/sets/complement2.cvc - regress0/sets/complement3.cvc - regress0/sets/cvc-sample.cvc - regress0/sets/dt-simp-mem.smt2 - regress0/sets/emptyset.smt2 - regress0/sets/eqtest.smt2 - regress0/sets/error1.smt2 - regress0/sets/error2.smt2 - regress0/sets/insert.smt2 - regress0/sets/int-real-univ-unsat.smt2 - regress0/sets/int-real-univ.smt2 - regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 - regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 - regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 - regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 - regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 - regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 - regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 - regress0/sets/mar2014/sharing-preregister.smt2 - regress0/sets/mar2014/small.smt2 - regress0/sets/mar2014/smaller.smt2 - regress0/sets/nonvar-univ.smt2 - regress0/sets/pre-proc-univ.smt2 - regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 - regress0/sets/sets-equal.smt2 - regress0/sets/sets-inter.smt2 - regress0/sets/sets-of-sets-subtypes.smt2 - regress0/sets/sets-poly-int-real.smt2 - regress0/sets/sets-poly-nonint.smt2 - regress0/sets/sets-sample.smt2 - regress0/sets/sets-sharing.smt2 - regress0/sets/sets-testlemma.smt2 - regress0/sets/sets-union.smt2 - regress0/sets/sharing-simp.smt2 - regress0/sets/union-1a-flip.smt2 - regress0/sets/union-1a.smt2 - regress0/sets/union-1b-flip.smt2 - regress0/sets/union-1b.smt2 - regress0/sets/union-2.smt2 - regress0/sets/univset-simp.smt2 - regress0/simple-lra.smt - regress0/simple-lra.smt2 - regress0/simple-rdl.smt - regress0/simple-rdl.smt2 - regress0/simple-uf.smt - regress0/simple-uf.smt2 - regress0/simple.cvc - regress0/simple.smt - regress0/simple2.smt - regress0/simplification_bug.smt - regress0/simplification_bug2.smt - regress0/smallcnf.cvc - regress0/smt2output.smt2 - regress0/strings/bug001.smt2 - regress0/strings/bug002.smt2 - regress0/strings/bug612.smt2 - regress0/strings/bug613.smt2 - regress0/strings/code-sat-neg-one.smt2 - regress0/strings/escchar.smt2 - regress0/strings/escchar_25.smt2 - regress0/strings/idof-rewrites.smt2 - regress0/strings/idof-sem.smt2 - regress0/strings/ilc-like.smt2 - regress0/strings/indexof-sym-simp.smt2 - regress0/strings/issue1189.smt2 - regress0/strings/leadingzero001.smt2 - regress0/strings/loop001.smt2 - regress0/strings/model001.smt2 - regress0/strings/norn-31.smt2 - regress0/strings/norn-simp-rew.smt2 - regress0/strings/repl-rewrites2.smt2 - regress0/strings/rewrites-v2.smt2 - regress0/strings/std2.6.1.smt2 - regress0/strings/str003.smt2 - regress0/strings/str004.smt2 - regress0/strings/str005.smt2 - regress0/strings/strings-charat.cvc - regress0/strings/strings-native-simple.cvc - regress0/strings/strip-endpoint-itos.smt2 - regress0/strings/substr-rewrites.smt2 - regress0/strings/type001.smt2 - regress0/strings/unsound-0908.smt2 - regress0/sygus/General_plus10.sy - regress0/sygus/aig-si.sy - regress0/sygus/c100.sy - regress0/sygus/ccp16.lus.sy - regress0/sygus/check-generic-red.sy - regress0/sygus/const-var-test.sy - regress0/sygus/dt-no-syntax.sy - regress0/sygus/let-ringer.sy - regress0/sygus/let-simp.sy - regress0/sygus/no-syntax-test-bool.sy - regress0/sygus/no-syntax-test.sy - regress0/sygus/parity-AIG-d0.sy - regress0/sygus/parse-bv-let.sy - regress0/sygus/real-si-all.sy - regress0/sygus/strings-unconstrained.sy - regress0/sygus/uminus_one.sy - regress0/test11.cvc - regress0/test9.cvc - regress0/tptp/ARI086=1.p - regress0/tptp/DAT001=1.p - regress0/tptp/KRS018+1.p - regress0/tptp/KRS063+1.p - regress0/tptp/MGT019+2.p - regress0/tptp/MGT041-2.p - regress0/tptp/PUZ131_1.p - regress0/tptp/SYN000=2.p - regress0/tptp/SYN000+1.p - regress0/tptp/SYN000+2.p - regress0/tptp/SYN000-1.p - regress0/tptp/SYN000-2.p - regress0/tptp/SYN000_1.p - regress0/tptp/SYN000_2.p - regress0/tptp/SYN075-1.p - regress0/tptp/tff0-arith.p - regress0/tptp/tff0.p - regress0/tptp/tptp_parser.p - regress0/tptp/tptp_parser10.p - regress0/tptp/tptp_parser2.p - regress0/tptp/tptp_parser3.p - regress0/tptp/tptp_parser4.p - regress0/tptp/tptp_parser5.p - regress0/tptp/tptp_parser6.p - regress0/tptp/tptp_parser7.p - regress0/tptp/tptp_parser8.p - regress0/tptp/tptp_parser9.p - regress0/uf/NEQ016_size5_reduced2a.smt - regress0/uf/NEQ016_size5_reduced2b.smt - regress0/uf/bool-pred-nested.smt2 - regress0/uf/ccredesign-fuzz.smt - regress0/uf/cnf-and-neg.smt2 - regress0/uf/cnf-iff-base.smt2 - regress0/uf/cnf-iff.smt2 - regress0/uf/cnf-ite.smt2 - regress0/uf/cnf_abc.smt2 - regress0/uf/dead_dnd002.smt - regress0/uf/eq_diamond1.smt - regress0/uf/eq_diamond14.reduced.smt - regress0/uf/eq_diamond14.reduced2.smt - regress0/uf/eq_diamond23.smt - regress0/uf/euf_simp01.smt - regress0/uf/euf_simp02.smt - regress0/uf/euf_simp03.smt - regress0/uf/euf_simp04.smt - regress0/uf/euf_simp05.smt - regress0/uf/euf_simp06.smt - regress0/uf/euf_simp08.smt - regress0/uf/euf_simp09.smt - regress0/uf/euf_simp10.smt - regress0/uf/euf_simp11.smt - regress0/uf/euf_simp12.smt - regress0/uf/euf_simp13.smt - regress0/uf/iso_brn001.smt - regress0/uf/pred.smt - regress0/uf/simple.01.cvc - regress0/uf/simple.02.cvc - regress0/uf/simple.03.cvc - regress0/uf/simple.04.cvc - regress0/uf20-03.cvc - regress0/uflia/check01.smt2 - regress0/uflia/check02.smt2 - regress0/uflia/check03.smt2 - regress0/uflia/check04.smt2 - regress0/uflia/error0.delta01.smt - regress0/uflia/error1.smt - regress0/uflia/error30.smt - regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2 - regress0/uflia/tiny.smt2 - regress0/uflia/xs-09-16-3-4-1-5.delta01.smt - regress0/uflia/xs-09-16-3-4-1-5.delta02.smt - regress0/uflia/xs-09-16-3-4-1-5.delta03.smt - regress0/uflia/xs-09-16-3-4-1-5.delta04.smt - regress0/uflra/bug293.cvc - regress0/uflra/bug449.smt - regress0/uflra/constants0.smt - regress0/uflra/fuzz01.smt - regress0/uflra/incorrect1.delta01.smt - regress0/uflra/incorrect1.delta02.smt - regress0/uflra/neq-deltacomp.smt - regress0/uflra/pb_real_10_0100_10_10.smt - regress0/uflra/pb_real_10_0100_10_11.smt - regress0/uflra/pb_real_10_0100_10_15.smt - regress0/uflra/pb_real_10_0100_10_16.smt - regress0/uflra/pb_real_10_0100_10_19.smt - regress0/uflra/pb_real_10_0200_10_22.smt - regress0/uflra/pb_real_10_0200_10_26.smt - regress0/uflra/pb_real_10_0200_10_29.smt - regress0/uflra/simple.01.cvc - regress0/uflra/simple.02.cvc - regress0/uflra/simple.03.cvc - regress0/uflra/simple.04.cvc - regress0/unconstrained/arith.smt2 - regress0/unconstrained/arith3.smt2 - regress0/unconstrained/arith4.smt2 - regress0/unconstrained/arith5.smt2 - regress0/unconstrained/arith6.smt2 - regress0/unconstrained/array1.smt2 - regress0/unconstrained/bvbool.smt2 - regress0/unconstrained/bvbool2.smt2 - regress0/unconstrained/bvbool3.smt2 - regress0/unconstrained/bvcmp.smt2 - regress0/unconstrained/bvconcat2.smt2 - regress0/unconstrained/bvext.smt2 - regress0/unconstrained/bvite.smt2 - regress0/unconstrained/bvmul.smt2 - regress0/unconstrained/bvmul2.smt2 - regress0/unconstrained/bvmul3.smt2 - regress0/unconstrained/bvnot.smt2 - regress0/unconstrained/bvsle.smt2 - regress0/unconstrained/bvsle2.smt2 - regress0/unconstrained/bvsle3.smt2 - regress0/unconstrained/bvsle4.smt2 - regress0/unconstrained/bvsle5.smt2 - regress0/unconstrained/bvslt.smt2 - regress0/unconstrained/bvslt2.smt2 - regress0/unconstrained/bvslt3.smt2 - regress0/unconstrained/bvslt4.smt2 - regress0/unconstrained/bvslt5.smt2 - regress0/unconstrained/bvule.smt2 - regress0/unconstrained/bvule2.smt2 - regress0/unconstrained/bvule3.smt2 - regress0/unconstrained/bvule4.smt2 - regress0/unconstrained/bvule5.smt2 - regress0/unconstrained/bvult.smt2 - regress0/unconstrained/bvult2.smt2 - regress0/unconstrained/bvult3.smt2 - regress0/unconstrained/bvult4.smt2 - regress0/unconstrained/bvult5.smt2 - regress0/unconstrained/geq.smt2 - regress0/unconstrained/gt.smt2 - regress0/unconstrained/ite.smt2 - regress0/unconstrained/leq.smt2 - regress0/unconstrained/lt.smt2 - regress0/unconstrained/mult1.smt2 - regress0/unconstrained/uf1.smt2 - regress0/unconstrained/xor.smt2 - regress0/wiki.01.cvc - regress0/wiki.02.cvc - regress0/wiki.03.cvc - regress0/wiki.04.cvc - regress0/wiki.05.cvc - regress0/wiki.06.cvc - regress0/wiki.07.cvc - regress0/wiki.08.cvc - regress0/wiki.09.cvc - regress0/wiki.10.cvc - regress0/wiki.11.cvc - regress0/wiki.12.cvc - regress0/wiki.13.cvc - regress0/wiki.14.cvc - regress0/wiki.15.cvc - regress0/wiki.16.cvc - regress0/wiki.17.cvc - regress0/wiki.18.cvc - regress0/wiki.19.cvc - regress0/wiki.20.cvc - regress0/wiki.21.cvc + regress0/arith/arith.01.cvc + regress0/arith/arith.02.cvc + regress0/arith/arith.03.cvc + regress0/arith/bug443.delta01.smt + regress0/arith/bug547.2.smt2 + regress0/arith/bug569.smt2 + regress0/arith/delta-minimized-row-vector-bug.smt + regress0/arith/div-chainable.smt2 + regress0/arith/div.01.smt2 + regress0/arith/div.02.smt2 + regress0/arith/div.04.smt2 + regress0/arith/div.05.smt2 + regress0/arith/div.07.smt2 + regress0/arith/fuzz_3-eq.smt + regress0/arith/integers/arith-int-042.cvc + regress0/arith/integers/arith-int-042.min.cvc + regress0/arith/leq.01.smt + regress0/arith/miplib.cvc + regress0/arith/miplib2.cvc + regress0/arith/miplib4.cvc + regress0/arith/miplibtrick.smt + regress0/arith/mod-simp.smt2 + regress0/arith/mod.01.smt2 + regress0/arith/mult.01.smt2 + regress0/arrayinuf_declare.smt2 + regress0/arrays/arrays0.smt2 + regress0/arrays/arrays1.smt2 + regress0/arrays/arrays2.smt2 + regress0/arrays/arrays3.smt2 + regress0/arrays/arrays4.smt2 + regress0/arrays/bool-array.smt2 + regress0/arrays/bug272.minimized.smt + regress0/arrays/bug272.smt + regress0/arrays/bug637.delta.smt2 + regress0/arrays/constarr.cvc + regress0/arrays/constarr.smt2 + regress0/arrays/constarr2.cvc + regress0/arrays/constarr2.smt2 + regress0/arrays/incorrect1.smt + regress0/arrays/incorrect10.smt + regress0/arrays/incorrect11.smt + regress0/arrays/incorrect2.minimized.smt + regress0/arrays/incorrect2.smt + regress0/arrays/incorrect3.smt + regress0/arrays/incorrect4.smt + regress0/arrays/incorrect5.smt + regress0/arrays/incorrect6.smt + regress0/arrays/incorrect7.smt + regress0/arrays/incorrect8.minimized.smt + regress0/arrays/incorrect8.smt + regress0/arrays/incorrect9.smt + regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smt + regress0/arrays/x2.smt + regress0/arrays/x3.smt + regress0/aufbv/array_rewrite_bug.smt + regress0/aufbv/bug00.smt + regress0/aufbv/bug338.smt2 + regress0/aufbv/bug347.smt + regress0/aufbv/bug451.smt + regress0/aufbv/bug509.smt + regress0/aufbv/bug580.delta.smt2 + regress0/aufbv/diseqprop.01.smt + regress0/aufbv/dubreva005ue.delta01.smt + regress0/aufbv/fifo32bc06k08.delta01.smt + regress0/aufbv/fuzz00.smt + regress0/aufbv/fuzz01.delta01.smt + regress0/aufbv/fuzz01.smt + regress0/aufbv/fuzz02.delta01.smt + regress0/aufbv/fuzz02.smt + regress0/aufbv/fuzz03.delta01.smt + regress0/aufbv/fuzz03.smt + regress0/aufbv/fuzz04.delta01.smt + regress0/aufbv/fuzz04.smt + regress0/aufbv/fuzz05.delta01.smt + regress0/aufbv/fuzz05.smt + regress0/aufbv/fuzz06.delta01.smt + regress0/aufbv/fuzz06.smt + regress0/aufbv/fuzz07.smt + regress0/aufbv/fuzz08.smt + regress0/aufbv/fuzz09.smt + regress0/aufbv/fuzz11.smt + regress0/aufbv/fuzz12.smt + regress0/aufbv/fuzz13.smt + regress0/aufbv/fuzz14.smt + regress0/aufbv/fuzz15.smt + regress0/aufbv/rewrite_bug.smt + regress0/aufbv/try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.delta01.smt + regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt + regress0/aufbv/wchains010ue.delta01.smt + regress0/aufbv/wchains010ue.delta02.smt + regress0/auflia/a17.smt + regress0/auflia/bug336.smt2 + regress0/auflia/error72.delta2.smt + regress0/auflia/fuzz-error1099.smt + regress0/auflia/fuzz-error232.smt + regress0/auflia/fuzz01.delta01.smt + regress0/auflia/fuzz02.smt + regress0/auflia/fuzz03.smt + regress0/auflia/fuzz04.smt + regress0/auflia/fuzz05.smt + regress0/auflia/x2.smt + regress0/boolean-prec.cvc + regress0/boolean-terms-bug-array.smt2 + regress0/boolean-terms-kernel1.smt2 + regress0/boolean-terms.cvc + regress0/bt-test-00.smt2 + regress0/bt-test-01.smt2 + regress0/bug1247.smt2 + regress0/bug161.smt + regress0/bug164.smt + regress0/bug167.smt + regress0/bug168.smt + regress0/bug187.smt2 + regress0/bug217.smt2 + regress0/bug220.smt2 + regress0/bug239.smt + regress0/bug274.cvc + regress0/bug288.smt + regress0/bug288b.smt + regress0/bug288c.smt + regress0/bug303.smt2 + regress0/bug310.cvc + regress0/bug32.cvc + regress0/bug322.cvc + regress0/bug322b.cvc + regress0/bug339.smt2 + regress0/bug365.smt2 + regress0/bug382.smt2 + regress0/bug383.smt2 + regress0/bug398.smt2 + regress0/bug421.smt2 + regress0/bug421b.smt2 + regress0/bug480.smt2 + regress0/bug484.smt2 + regress0/bug486.cvc + regress0/bug49.smt + regress0/bug512.minimized.smt2 + regress0/bug521.minimized.smt2 + regress0/bug522.smt2 + regress0/bug528a.smt2 + regress0/bug541.smt2 + regress0/bug544.smt2 + regress0/bug548a.smt2 + regress0/bug576.smt2 + regress0/bug576a.smt2 + regress0/bug578.smt2 + regress0/bug586.cvc + regress0/bug595.cvc + regress0/bug596.cvc + regress0/bug596b.cvc + regress0/bug605.cvc + regress0/bug639.smt2 + regress0/buggy-ite.smt2 + regress0/bv/bool-to-bv.smt2 + regress0/bv/bug260a.smt + regress0/bv/bug260b.smt + regress0/bv/bug440.smt + regress0/bv/bug733.smt2 + regress0/bv/bug734.smt2 + regress0/bv/bv-abstr-bug.smt2 + regress0/bv/bv-abstr-bug2.smt2 + regress0/bv/bv-int-collapse1.smt2 + regress0/bv/bv-int-collapse2.smt2 + regress0/bv/bv-options1.smt2 + regress0/bv/bv-options2.smt2 + regress0/bv/bv-options3.smt2 + regress0/bv/bv-options4.smt2 + regress0/bv/bv-to-bool.smt + regress0/bv/bv2nat-ground-c.smt2 + regress0/bv/bv2nat-simp-range.smt2 + regress0/bv/bvmul-pow2-only.smt2 + regress0/bv/bvsimple.cvc + regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt + regress0/bv/core/a78test0002.smt + regress0/bv/core/a95test0002.smt + regress0/bv/core/bitvec0.smt + regress0/bv/core/bitvec2.smt + regress0/bv/core/bitvec5.smt + regress0/bv/core/bitvec7.smt + regress0/bv/core/bv_eq_diamond10.smt + regress0/bv/core/concat-merge-0.smt + regress0/bv/core/concat-merge-1.smt + regress0/bv/core/concat-merge-2.smt + regress0/bv/core/concat-merge-3.smt + regress0/bv/core/equality-00.smt + regress0/bv/core/equality-01.smt + regress0/bv/core/equality-02.smt + regress0/bv/core/equality-05.smt + regress0/bv/core/extract-concat-0.smt + regress0/bv/core/extract-concat-1.smt + regress0/bv/core/extract-concat-10.smt + regress0/bv/core/extract-concat-11.smt + regress0/bv/core/extract-concat-2.smt + regress0/bv/core/extract-concat-3.smt + regress0/bv/core/extract-concat-4.smt + regress0/bv/core/extract-concat-5.smt + regress0/bv/core/extract-concat-6.smt + regress0/bv/core/extract-concat-7.smt + regress0/bv/core/extract-concat-8.smt + regress0/bv/core/extract-concat-9.smt + regress0/bv/core/extract-constant.smt + regress0/bv/core/extract-extract-0.smt + regress0/bv/core/extract-extract-1.smt + regress0/bv/core/extract-extract-10.smt + regress0/bv/core/extract-extract-11.smt + regress0/bv/core/extract-extract-2.smt + regress0/bv/core/extract-extract-3.smt + regress0/bv/core/extract-extract-4.smt + regress0/bv/core/extract-extract-5.smt + regress0/bv/core/extract-extract-6.smt + regress0/bv/core/extract-extract-7.smt + regress0/bv/core/extract-extract-8.smt + regress0/bv/core/extract-extract-9.smt + regress0/bv/core/extract-whole-0.smt + regress0/bv/core/extract-whole-1.smt + regress0/bv/core/extract-whole-2.smt + regress0/bv/core/extract-whole-3.smt + regress0/bv/core/extract-whole-4.smt + regress0/bv/core/slice-01.smt + regress0/bv/core/slice-02.smt + regress0/bv/core/slice-03.smt + regress0/bv/core/slice-04.smt + regress0/bv/core/slice-05.smt + regress0/bv/core/slice-06.smt + regress0/bv/core/slice-07.smt + regress0/bv/core/slice-08.smt + regress0/bv/core/slice-09.smt + regress0/bv/core/slice-10.smt + regress0/bv/core/slice-11.smt + regress0/bv/core/slice-12.smt + regress0/bv/core/slice-13.smt + regress0/bv/core/slice-14.smt + regress0/bv/core/slice-15.smt + regress0/bv/core/slice-16.smt + regress0/bv/core/slice-17.smt + regress0/bv/core/slice-18.smt + regress0/bv/core/slice-19.smt + regress0/bv/core/slice-20.smt + regress0/bv/divtest_2_5.smt2 + regress0/bv/divtest_2_6.smt2 + regress0/bv/eager-inc-cryptominisat.smt2 + regress0/bv/fuzz01.smt + regress0/bv/fuzz02.delta01.smt + regress0/bv/fuzz02.smt + regress0/bv/fuzz03.smt + regress0/bv/fuzz04.smt + regress0/bv/fuzz05.smt + regress0/bv/fuzz06.smt + regress0/bv/fuzz07.smt + regress0/bv/fuzz08.smt + regress0/bv/fuzz09.smt + regress0/bv/fuzz10.smt + regress0/bv/fuzz11.smt + regress0/bv/fuzz12.smt + regress0/bv/fuzz13.smt + regress0/bv/fuzz14.smt + regress0/bv/fuzz16.delta01.smt + regress0/bv/fuzz17.delta01.smt + regress0/bv/fuzz18.delta01.smt + regress0/bv/fuzz18.delta02.smt + regress0/bv/fuzz18.delta03.smt + regress0/bv/fuzz18.smt + regress0/bv/fuzz19.delta01.smt + regress0/bv/fuzz19.smt + regress0/bv/fuzz20.delta01.smt + regress0/bv/fuzz20.smt + regress0/bv/fuzz21.delta01.smt + regress0/bv/fuzz21.smt + regress0/bv/fuzz22.delta01.smt + regress0/bv/fuzz22.smt + regress0/bv/fuzz23.delta01.smt + regress0/bv/fuzz23.smt + regress0/bv/fuzz24.delta01.smt + regress0/bv/fuzz24.smt + regress0/bv/fuzz25.delta01.smt + regress0/bv/fuzz25.smt + regress0/bv/fuzz26.delta01.smt + regress0/bv/fuzz26.smt + regress0/bv/fuzz27.delta01.smt + regress0/bv/fuzz27.smt + regress0/bv/fuzz28.delta01.smt + regress0/bv/fuzz28.smt + regress0/bv/fuzz29.delta01.smt + regress0/bv/fuzz29.smt + regress0/bv/fuzz30.delta01.smt + regress0/bv/fuzz30.smt + regress0/bv/fuzz31.delta01.smt + regress0/bv/fuzz31.smt + regress0/bv/fuzz32.delta01.smt + regress0/bv/fuzz32.smt + regress0/bv/fuzz33.delta01.smt + regress0/bv/fuzz33.smt + regress0/bv/fuzz34.delta01.smt + regress0/bv/fuzz35.delta01.smt + regress0/bv/fuzz35.smt + regress0/bv/fuzz36.delta01.smt + regress0/bv/fuzz36.smt + regress0/bv/fuzz37.delta01.smt + regress0/bv/fuzz37.smt + regress0/bv/fuzz38.delta01.smt + regress0/bv/fuzz39.delta01.smt + regress0/bv/fuzz39.smt + regress0/bv/fuzz40.delta01.smt + regress0/bv/fuzz40.smt + regress0/bv/fuzz41.smt + regress0/bv/mul-neg-unsat.smt2 + regress0/bv/mul-negpow2.smt2 + regress0/bv/mult-pow2-negative.smt2 + regress0/bv/sizecheck.cvc + regress0/bv/smtcompbug.smt + regress0/bv/test-bv_intro_pow2.smt2 + regress0/bv/unsound1-reduced.smt2 + regress0/chained-equality.smt2 + regress0/constant-rewrite.smt + regress0/cvc3.userdoc.01.cvc + regress0/cvc3.userdoc.02.cvc + regress0/cvc3.userdoc.03.cvc + regress0/cvc3.userdoc.04.cvc + regress0/cvc3.userdoc.05.cvc + regress0/cvc3.userdoc.06.cvc + regress0/datatypes/Test1-tup-mp.cvc + regress0/datatypes/boolean-equality.cvc + regress0/datatypes/boolean-terms-datatype.cvc + regress0/datatypes/boolean-terms-parametric-datatype-1.cvc + regress0/datatypes/boolean-terms-parametric-datatype-2.cvc + regress0/datatypes/boolean-terms-record.cvc + regress0/datatypes/boolean-terms-rewrite.cvc + regress0/datatypes/boolean-terms-tuple.cvc + regress0/datatypes/bug286.cvc + regress0/datatypes/bug438.cvc + regress0/datatypes/bug438b.cvc + regress0/datatypes/bug597-rbt.smt2 + regress0/datatypes/bug604.smt2 + regress0/datatypes/bug625.smt2 + regress0/datatypes/cdt-model-cade15.smt2 + regress0/datatypes/cdt-non-canon-stream.smt2 + regress0/datatypes/coda_simp_model.smt2 + regress0/datatypes/conqueue-dt-enum-iloop.smt2 + regress0/datatypes/datatype.cvc + regress0/datatypes/datatype0.cvc + regress0/datatypes/datatype1.cvc + regress0/datatypes/datatype13.cvc + regress0/datatypes/datatype2.cvc + regress0/datatypes/datatype3.cvc + regress0/datatypes/datatype4.cvc + regress0/datatypes/dt-2.6.smt2 + regress0/datatypes/dt-match-pat-param-2.6.smt2 + regress0/datatypes/dt-param-2.6.smt2 + regress0/datatypes/dt-param-card4-bool-sat.smt2 + regress0/datatypes/dt-sel-2.6.smt2 + regress0/datatypes/empty_tuprec.cvc + regress0/datatypes/example-dailler-min.smt2 + regress0/datatypes/is_test.smt2 + regress0/datatypes/issue1433.smt2 + regress0/datatypes/jsat-2.6.smt2 + regress0/datatypes/model-subterms-min.smt2 + regress0/datatypes/mutually-recursive.cvc + regress0/datatypes/pair-bool-bool.cvc + regress0/datatypes/pair-real-bool.smt2 + regress0/datatypes/rec1.cvc + regress0/datatypes/rec2.cvc + regress0/datatypes/rec4.cvc + regress0/datatypes/rewriter.cvc + regress0/datatypes/sc-cdt1.smt2 + regress0/datatypes/some-boolean-tests.cvc + regress0/datatypes/stream-singleton.smt2 + regress0/datatypes/tenum-bug.smt2 + regress0/datatypes/tuple-model.cvc + regress0/datatypes/tuple-no-clash.cvc + regress0/datatypes/tuple-record-bug.cvc + regress0/datatypes/tuple.cvc + regress0/datatypes/tuples-empty.smt2 + regress0/datatypes/tuples-multitype.smt2 + regress0/datatypes/typed_v10l30054.cvc + regress0/datatypes/typed_v1l80005.cvc + regress0/datatypes/typed_v2l30079.cvc + regress0/datatypes/typed_v3l20092.cvc + regress0/datatypes/typed_v5l30069.cvc + regress0/datatypes/v10l40099.cvc + regress0/datatypes/v2l40025.cvc + regress0/datatypes/v3l60006.cvc + regress0/datatypes/v5l30058.cvc + regress0/datatypes/wrong-sel-simp.cvc + regress0/decision/aufbv-fuzz01.smt + regress0/decision/bitvec0.delta01.smt + regress0/decision/bitvec0.smt + regress0/decision/bitvec5.smt + regress0/decision/bug347.smt + regress0/decision/bug374a.smt + regress0/decision/bug374b.smt2 + regress0/decision/error122.delta01.smt + regress0/decision/error122.smt + regress0/decision/error20.delta01.smt + regress0/decision/error20.smt + regress0/decision/error3.delta01.smt + regress0/decision/pp-regfile.delta01.smt + regress0/decision/pp-regfile.delta02.smt + regress0/decision/quant-ex1.smt2 + regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt + regress0/decision/wchains010ue.delta02.smt + regress0/declare-fun-is-match.smt2 + regress0/declare-funs.smt2 + regress0/distinct.smt + regress0/expect/scrub.01.smt + regress0/expect/scrub.02.smt + regress0/expect/scrub.03.smt2 + regress0/expect/scrub.04.smt2 + regress0/expect/scrub.06.cvc + regress0/expect/scrub.08.sy + regress0/expect/scrub.09.p + regress0/flet.smt + regress0/flet2.smt + regress0/fmf/Arrow_Order-smtlib.778341.smt + regress0/fmf/QEpres-uf.855035.smt + regress0/fmf/array_card.smt2 + regress0/fmf/bounded_sets.smt2 + regress0/fmf/bug-041417-set-options.cvc + regress0/fmf/bug652.smt2 + regress0/fmf/bug782.smt2 + regress0/fmf/cruanes-no-minimal-unk.smt2 + regress0/fmf/fc-simple.smt2 + regress0/fmf/fc-unsat-pent.smt2 + regress0/fmf/fc-unsat-tot-2.smt2 + regress0/fmf/fd-false.smt2 + regress0/fmf/fmc_unsound_model.smt2 + regress0/fmf/fmf-strange-bounds-2.smt2 + regress0/fmf/forall_unit_data2.smt2 + regress0/fmf/krs-sat.smt2 + regress0/fmf/no-minimal-sat.smt2 + regress0/fmf/quant_real_univ.cvc + regress0/fmf/sat-logic.smt2 + regress0/fmf/sc_bad_model_1221.smt2 + regress0/fmf/syn002-si-real-int.smt2 + regress0/fmf/tail_rec.smt2 + regress0/fp/simple.smt2 + regress0/fuzz_1.smt + regress0/fuzz_3.smt + regress0/get-value-incremental.smt2 + regress0/get-value-ints.smt2 + regress0/get-value-reals-ints.smt2 + regress0/get-value-reals.smt2 + regress0/ho/apply-collapse-sat.smt2 + regress0/ho/apply-collapse-unsat.smt2 + regress0/ho/cong-full-apply.smt2 + regress0/ho/cong.smt2 + regress0/ho/declare-fun-variants.smt2 + regress0/ho/def-fun-flatten.smt2 + regress0/ho/ext-finite-unsat.smt2 + regress0/ho/ext-ho-nested-lambda-model.smt2 + regress0/ho/ext-ho.smt2 + regress0/ho/ext-sat-partial-eval.smt2 + regress0/ho/ext-sat.smt2 + regress0/ho/finite-fun-ext.smt2 + regress0/ho/fta0144-alpha-eq.smt2 + regress0/ho/ho-match-fun-suffix.smt2 + regress0/ho/ho-matching-enum.smt2 + regress0/ho/ho-matching-nested-app.smt2 + regress0/ho/ite-apply-eq.smt2 + regress0/ho/lambda-equality-non-canon.smt2 + regress0/ho/modulo-func-equality.smt2 + regress0/ho/simple-matching-partial.smt2 + regress0/ho/simple-matching.smt2 + regress0/ho/trans.smt2 + regress0/hung10_itesdk_output1.smt2 + regress0/hung10_itesdk_output2.smt2 + regress0/hung13sdk_output1.smt2 + regress0/hung13sdk_output2.smt2 + regress0/ineq_basic.smt + regress0/ineq_slack.smt + regress0/issue1063-overloading-dt-cons.smt2 + regress0/issue1063-overloading-dt-fun.smt2 + regress0/issue1063-overloading-dt-sel.smt2 + regress0/ite.cvc + regress0/ite2.smt2 + regress0/ite3.smt2 + regress0/ite4.smt2 + regress0/ite_real_int_type.smt + regress0/ite_real_valid.smt + regress0/lang_opts_2_5.smt2 + regress0/lang_opts_2_6_1.smt2 + regress0/lemmas/clocksynchro_5clocks.main_invar.base.model.smt + regress0/lemmas/fs_not_sc_seen.induction.smt + regress0/lemmas/mode_cntrl.induction.smt + regress0/lemmas/sc_init_frame_gap.induction.smt + regress0/let.cvc + regress0/let.smt + regress0/let2.smt + regress0/logops.01.cvc + regress0/logops.02.cvc + regress0/logops.03.cvc + regress0/logops.04.cvc + regress0/logops.05.cvc + regress0/model-core.smt2 + regress0/nl/coeff-sat.smt2 + regress0/nl/magnitude-wrong-1020-m.smt2 + regress0/nl/mult-po.smt2 + regress0/nl/nia-wrong-tl.smt2 + regress0/nl/nta/cos-sig-value.smt2 + regress0/nl/nta/exp-n0.5-lb.smt2 + regress0/nl/nta/exp-n0.5-ub.smt2 + regress0/nl/nta/exp1-ub.smt2 + regress0/nl/nta/real-pi.smt2 + regress0/nl/nta/sin-sym.smt2 + regress0/nl/nta/sqrt-simple.smt2 + regress0/nl/nta/tan-rewrite.smt2 + regress0/nl/real-as-int.smt2 + regress0/nl/real-div-ufnra.smt2 + regress0/nl/subs0-unsat-confirm.smt2 + regress0/nl/very-easy-sat.smt2 + regress0/nl/very-simple-unsat.smt2 + regress0/parallel-let.smt2 + regress0/parser/as.smt2 + regress0/parser/constraint.smt2 + regress0/parser/declarefun-emptyset-uf.smt2 + regress0/parser/shadow_fun_symbol_all.smt2 + regress0/parser/shadow_fun_symbol_nirat.smt2 + regress0/parser/strings20.smt2 + regress0/parser/strings25.smt2 + regress0/precedence/and-not.cvc + regress0/precedence/and-xor.cvc + regress0/precedence/bool-cmp.cvc + regress0/precedence/cmp-plus.cvc + regress0/precedence/eq-fun.cvc + regress0/precedence/iff-assoc.cvc + regress0/precedence/iff-implies.cvc + regress0/precedence/implies-assoc.cvc + regress0/precedence/implies-iff.cvc + regress0/precedence/implies-or.cvc + regress0/precedence/not-and.cvc + regress0/precedence/not-eq.cvc + regress0/precedence/or-implies.cvc + regress0/precedence/or-xor.cvc + regress0/precedence/plus-mult.cvc + regress0/precedence/xor-and.cvc + regress0/precedence/xor-assoc.cvc + regress0/precedence/xor-or.cvc + regress0/preprocess/preprocess_00.cvc + regress0/preprocess/preprocess_01.cvc + regress0/preprocess/preprocess_02.cvc + regress0/preprocess/preprocess_03.cvc + regress0/preprocess/preprocess_04.cvc + regress0/preprocess/preprocess_05.cvc + regress0/preprocess/preprocess_06.cvc + regress0/preprocess/preprocess_07.cvc + regress0/preprocess/preprocess_08.cvc + regress0/preprocess/preprocess_09.cvc + regress0/preprocess/preprocess_10.cvc + regress0/preprocess/preprocess_11.cvc + regress0/preprocess/preprocess_12.cvc + regress0/preprocess/preprocess_13.cvc + regress0/preprocess/preprocess_14.cvc + regress0/preprocess/preprocess_15.cvc + regress0/print_lambda.cvc + regress0/push-pop/boolean/fuzz_12.smt2 + regress0/push-pop/boolean/fuzz_13.smt2 + regress0/push-pop/boolean/fuzz_14.smt2 + regress0/push-pop/boolean/fuzz_18.smt2 + regress0/push-pop/boolean/fuzz_2.smt2 + regress0/push-pop/boolean/fuzz_21.smt2 + regress0/push-pop/boolean/fuzz_22.smt2 + regress0/push-pop/boolean/fuzz_27.smt2 + regress0/push-pop/boolean/fuzz_3.smt2 + regress0/push-pop/boolean/fuzz_31.smt2 + regress0/push-pop/boolean/fuzz_33.smt2 + regress0/push-pop/boolean/fuzz_36.smt2 + regress0/push-pop/boolean/fuzz_38.smt2 + regress0/push-pop/boolean/fuzz_46.smt2 + regress0/push-pop/boolean/fuzz_47.smt2 + regress0/push-pop/boolean/fuzz_48.smt2 + regress0/push-pop/boolean/fuzz_49.smt2 + regress0/push-pop/boolean/fuzz_50.smt2 + regress0/push-pop/bug1990.smt2 + regress0/push-pop/bug233.cvc + regress0/push-pop/bug654-dd.smt2 + regress0/push-pop/bug691.smt2 + regress0/push-pop/bug821-check_sat_assuming.smt2 + regress0/push-pop/bug821.smt2 + regress0/push-pop/inc-define.smt2 + regress0/push-pop/inc-double-u.smt2 + regress0/push-pop/incremental-subst-bug.cvc + regress0/push-pop/issue1986.smt2 + regress0/push-pop/issue2137.min.smt2 + regress0/push-pop/quant-fun-proc-unfd.smt2 + regress0/push-pop/simple_unsat_cores.smt2 + regress0/push-pop/test.00.cvc + regress0/push-pop/test.01.cvc + regress0/push-pop/tiny_bug.smt2 + regress0/push-pop/units.cvc + regress0/quantifiers/ARI176e1.smt2 + regress0/quantifiers/agg-rew-test-cf.smt2 + regress0/quantifiers/agg-rew-test.smt2 + regress0/quantifiers/ari056.smt2 + regress0/quantifiers/bug269.smt2 + regress0/quantifiers/bug290.smt2 + regress0/quantifiers/bug291.smt2 + regress0/quantifiers/bug749-rounding.smt2 + regress0/quantifiers/cbqi-lia-dt-simp.smt2 + regress0/quantifiers/cegqi-nl-simp.cvc + regress0/quantifiers/cegqi-nl-sq.smt2 + regress0/quantifiers/clock-10.smt2 + regress0/quantifiers/clock-3.smt2 + regress0/quantifiers/cond-var-elim-binary.smt2 + regress0/quantifiers/delta-simp.smt2 + regress0/quantifiers/double-pattern.smt2 + regress0/quantifiers/ex3.smt2 + regress0/quantifiers/ex6.smt2 + regress0/quantifiers/floor.smt2 + regress0/quantifiers/horn-ground-pre-post.smt2 + regress0/quantifiers/is-even-pred.smt2 + regress0/quantifiers/is-int.smt2 + regress0/quantifiers/issue1805.smt2 + regress0/quantifiers/issue2031-bv-var-elim.smt2 + regress0/quantifiers/issue2033-macro-arith.smt2 + regress0/quantifiers/lra-triv-gn.smt2 + regress0/quantifiers/macros-int-real.smt2 + regress0/quantifiers/macros-real-arg.smt2 + regress0/quantifiers/matching-lia-1arg.smt2 + regress0/quantifiers/mix-complete-strat.smt2 + regress0/quantifiers/mix-match.smt2 + regress0/quantifiers/mix-simp.smt2 + regress0/quantifiers/nested-delta.smt2 + regress0/quantifiers/nested-inf.smt2 + regress0/quantifiers/partial-trigger.smt2 + regress0/quantifiers/pure_dt_cbqi.smt2 + regress0/quantifiers/qbv-inequality2.smt2 + regress0/quantifiers/qbv-simp.smt2 + regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 + regress0/quantifiers/qbv-test-invert-bvand-neq.smt2 + regress0/quantifiers/qbv-test-invert-bvand.smt2 + regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2 + regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2 + regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 + regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 + regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2 + regress0/quantifiers/qbv-test-invert-bvor-neq.smt2 + regress0/quantifiers/qbv-test-invert-bvor.smt2 + regress0/quantifiers/qbv-test-invert-bvshl-0.smt2 + regress0/quantifiers/qbv-test-invert-bvult-1.smt2 + regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2 + regress0/quantifiers/qbv-test-invert-bvxor.smt2 + regress0/quantifiers/qbv-test-invert-concat-0.smt2 + regress0/quantifiers/qbv-test-invert-concat-1.smt2 + regress0/quantifiers/qbv-test-invert-sign-extend.smt2 + regress0/quantifiers/qcf-rel-dom-opt.smt2 + regress0/quantifiers/rew-to-scala.smt2 + regress0/quantifiers/simp-len.smt2 + regress0/quantifiers/simp-typ-test.smt2 + regress0/queries0.cvc + regress0/rec-fun-const-parse-bug.smt2 + regress0/rels/addr_book_0.cvc + regress0/rels/atom_univ2.cvc + regress0/rels/card_transpose.cvc + regress0/rels/iden_0.cvc + regress0/rels/iden_1.cvc + regress0/rels/join-eq-u-sat.cvc + regress0/rels/join-eq-u.cvc + regress0/rels/joinImg_0.cvc + regress0/rels/oneLoc_no_quant-int_0_1.cvc + regress0/rels/rel_1tup_0.cvc + regress0/rels/rel_complex_0.cvc + regress0/rels/rel_complex_1.cvc + regress0/rels/rel_conflict_0.cvc + regress0/rels/rel_join_0.cvc + regress0/rels/rel_join_0_1.cvc + regress0/rels/rel_join_1.cvc + regress0/rels/rel_join_1_1.cvc + regress0/rels/rel_join_2.cvc + regress0/rels/rel_join_2_1.cvc + regress0/rels/rel_join_3.cvc + regress0/rels/rel_join_3_1.cvc + regress0/rels/rel_join_4.cvc + regress0/rels/rel_join_5.cvc + regress0/rels/rel_join_6.cvc + regress0/rels/rel_join_7.cvc + regress0/rels/rel_product_0.cvc + regress0/rels/rel_product_0_1.cvc + regress0/rels/rel_product_1.cvc + regress0/rels/rel_product_1_1.cvc + regress0/rels/rel_symbolic_1.cvc + regress0/rels/rel_symbolic_1_1.cvc + regress0/rels/rel_symbolic_2_1.cvc + regress0/rels/rel_symbolic_3_1.cvc + regress0/rels/rel_tc_11.cvc + regress0/rels/rel_tc_2_1.cvc + regress0/rels/rel_tc_3.cvc + regress0/rels/rel_tc_3_1.cvc + regress0/rels/rel_tc_7.cvc + regress0/rels/rel_tc_8.cvc + regress0/rels/rel_tp_3_1.cvc + regress0/rels/rel_tp_join_0.cvc + regress0/rels/rel_tp_join_1.cvc + regress0/rels/rel_tp_join_2.cvc + regress0/rels/rel_tp_join_3.cvc + regress0/rels/rel_tp_join_eq_0.cvc + regress0/rels/rel_tp_join_int_0.cvc + regress0/rels/rel_tp_join_pro_0.cvc + regress0/rels/rel_tp_join_var_0.cvc + regress0/rels/rel_transpose_0.cvc + regress0/rels/rel_transpose_1.cvc + regress0/rels/rel_transpose_1_1.cvc + regress0/rels/rel_transpose_3.cvc + regress0/rels/rel_transpose_4.cvc + regress0/rels/rel_transpose_5.cvc + regress0/rels/rel_transpose_6.cvc + regress0/rels/rel_transpose_7.cvc + regress0/rels/relations-ops.smt2 + regress0/rels/rels-sharing-simp.cvc + regress0/reset-assertions.smt2 + regress0/rewriterules/datatypes.smt2 + regress0/rewriterules/length_trick.smt2 + regress0/rewriterules/native_arrays.smt2 + regress0/rewriterules/relation.smt2 + regress0/rewriterules/simulate_rewriting.smt2 + regress0/sep/dispose-1.smt2 + regress0/sep/dup-nemp.smt2 + regress0/sep/nemp.smt2 + regress0/sep/nil-no-elim.smt2 + regress0/sep/nspatial-simp.smt2 + regress0/sep/pto-01.smt2 + regress0/sep/pto-02.smt2 + regress0/sep/sep-01.smt2 + regress0/sep/sep-plus1.smt2 + regress0/sep/sep-simp-unsat-emp.smt2 + regress0/sep/skolem_emp.smt2 + regress0/sep/trees-1.smt2 + regress0/sep/wand-crash.smt2 + regress0/sets/abt-min.smt2 + regress0/sets/abt-te-exh.smt2 + regress0/sets/abt-te-exh2.smt2 + regress0/sets/card-2.smt2 + regress0/sets/card-3sets.cvc + regress0/sets/card.smt2 + regress0/sets/card3-ground.smt2 + regress0/sets/complement.cvc + regress0/sets/complement2.cvc + regress0/sets/complement3.cvc + regress0/sets/cvc-sample.cvc + regress0/sets/dt-simp-mem.smt2 + regress0/sets/emptyset.smt2 + regress0/sets/eqtest.smt2 + regress0/sets/error1.smt2 + regress0/sets/error2.smt2 + regress0/sets/insert.smt2 + regress0/sets/int-real-univ-unsat.smt2 + regress0/sets/int-real-univ.smt2 + regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 + regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 + regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 + regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 + regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 + regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 + regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 + regress0/sets/mar2014/sharing-preregister.smt2 + regress0/sets/mar2014/small.smt2 + regress0/sets/mar2014/smaller.smt2 + regress0/sets/nonvar-univ.smt2 + regress0/sets/pre-proc-univ.smt2 + regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 + regress0/sets/sets-equal.smt2 + regress0/sets/sets-inter.smt2 + regress0/sets/sets-of-sets-subtypes.smt2 + regress0/sets/sets-poly-int-real.smt2 + regress0/sets/sets-poly-nonint.smt2 + regress0/sets/sets-sample.smt2 + regress0/sets/sets-sharing.smt2 + regress0/sets/sets-testlemma.smt2 + regress0/sets/sets-union.smt2 + regress0/sets/sharing-simp.smt2 + regress0/sets/union-1a-flip.smt2 + regress0/sets/union-1a.smt2 + regress0/sets/union-1b-flip.smt2 + regress0/sets/union-1b.smt2 + regress0/sets/union-2.smt2 + regress0/sets/univset-simp.smt2 + regress0/simple-lra.smt + regress0/simple-lra.smt2 + regress0/simple-rdl.smt + regress0/simple-rdl.smt2 + regress0/simple-uf.smt + regress0/simple-uf.smt2 + regress0/simple.cvc + regress0/simple.smt + regress0/simple2.smt + regress0/simplification_bug.smt + regress0/simplification_bug2.smt + regress0/smallcnf.cvc + regress0/smt2output.smt2 + regress0/strings/bug001.smt2 + regress0/strings/bug002.smt2 + regress0/strings/bug612.smt2 + regress0/strings/bug613.smt2 + regress0/strings/code-sat-neg-one.smt2 + regress0/strings/escchar.smt2 + regress0/strings/escchar_25.smt2 + regress0/strings/idof-rewrites.smt2 + regress0/strings/idof-sem.smt2 + regress0/strings/ilc-like.smt2 + regress0/strings/indexof-sym-simp.smt2 + regress0/strings/issue1189.smt2 + regress0/strings/leadingzero001.smt2 + regress0/strings/loop001.smt2 + regress0/strings/model001.smt2 + regress0/strings/norn-31.smt2 + regress0/strings/norn-simp-rew.smt2 + regress0/strings/repl-rewrites2.smt2 + regress0/strings/rewrites-v2.smt2 + regress0/strings/std2.6.1.smt2 + regress0/strings/str003.smt2 + regress0/strings/str004.smt2 + regress0/strings/str005.smt2 + regress0/strings/strings-charat.cvc + regress0/strings/strings-native-simple.cvc + regress0/strings/strip-endpoint-itos.smt2 + regress0/strings/substr-rewrites.smt2 + regress0/strings/type001.smt2 + regress0/strings/unsound-0908.smt2 + regress0/sygus/General_plus10.sy + regress0/sygus/aig-si.sy + regress0/sygus/c100.sy + regress0/sygus/ccp16.lus.sy + regress0/sygus/check-generic-red.sy + regress0/sygus/const-var-test.sy + regress0/sygus/dt-no-syntax.sy + regress0/sygus/let-ringer.sy + regress0/sygus/let-simp.sy + regress0/sygus/no-syntax-test-bool.sy + regress0/sygus/no-syntax-test.sy + regress0/sygus/parity-AIG-d0.sy + regress0/sygus/parse-bv-let.sy + regress0/sygus/real-si-all.sy + regress0/sygus/strings-unconstrained.sy + regress0/sygus/uminus_one.sy + regress0/test11.cvc + regress0/test9.cvc + regress0/tptp/ARI086=1.p + regress0/tptp/DAT001=1.p + regress0/tptp/KRS018+1.p + regress0/tptp/KRS063+1.p + regress0/tptp/MGT019+2.p + regress0/tptp/MGT041-2.p + regress0/tptp/PUZ131_1.p + regress0/tptp/SYN000+1.p + regress0/tptp/SYN000+2.p + regress0/tptp/SYN000-1.p + regress0/tptp/SYN000-2.p + regress0/tptp/SYN000=2.p + regress0/tptp/SYN000_1.p + regress0/tptp/SYN000_2.p + regress0/tptp/SYN075-1.p + regress0/tptp/tff0-arith.p + regress0/tptp/tff0.p + regress0/tptp/tptp_parser.p + regress0/tptp/tptp_parser10.p + regress0/tptp/tptp_parser2.p + regress0/tptp/tptp_parser3.p + regress0/tptp/tptp_parser4.p + regress0/tptp/tptp_parser5.p + regress0/tptp/tptp_parser6.p + regress0/tptp/tptp_parser7.p + regress0/tptp/tptp_parser8.p + regress0/tptp/tptp_parser9.p + regress0/uf/NEQ016_size5_reduced2a.smt + regress0/uf/NEQ016_size5_reduced2b.smt + regress0/uf/bool-pred-nested.smt2 + regress0/uf/ccredesign-fuzz.smt + regress0/uf/cnf-and-neg.smt2 + regress0/uf/cnf-iff-base.smt2 + regress0/uf/cnf-iff.smt2 + regress0/uf/cnf-ite.smt2 + regress0/uf/cnf_abc.smt2 + regress0/uf/dead_dnd002.smt + regress0/uf/eq_diamond1.smt + regress0/uf/eq_diamond14.reduced.smt + regress0/uf/eq_diamond14.reduced2.smt + regress0/uf/eq_diamond23.smt + regress0/uf/euf_simp01.smt + regress0/uf/euf_simp02.smt + regress0/uf/euf_simp03.smt + regress0/uf/euf_simp04.smt + regress0/uf/euf_simp05.smt + regress0/uf/euf_simp06.smt + regress0/uf/euf_simp08.smt + regress0/uf/euf_simp09.smt + regress0/uf/euf_simp10.smt + regress0/uf/euf_simp11.smt + regress0/uf/euf_simp12.smt + regress0/uf/euf_simp13.smt + regress0/uf/iso_brn001.smt + regress0/uf/pred.smt + regress0/uf/simple.01.cvc + regress0/uf/simple.02.cvc + regress0/uf/simple.03.cvc + regress0/uf/simple.04.cvc + regress0/uf20-03.cvc + regress0/uflia/check01.smt2 + regress0/uflia/check02.smt2 + regress0/uflia/check03.smt2 + regress0/uflia/check04.smt2 + regress0/uflia/error0.delta01.smt + regress0/uflia/error1.smt + regress0/uflia/error30.smt + regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2 + regress0/uflia/tiny.smt2 + regress0/uflia/xs-09-16-3-4-1-5.delta01.smt + regress0/uflia/xs-09-16-3-4-1-5.delta02.smt + regress0/uflia/xs-09-16-3-4-1-5.delta03.smt + regress0/uflia/xs-09-16-3-4-1-5.delta04.smt + regress0/uflra/bug293.cvc + regress0/uflra/bug449.smt + regress0/uflra/constants0.smt + regress0/uflra/fuzz01.smt + regress0/uflra/incorrect1.delta01.smt + regress0/uflra/incorrect1.delta02.smt + regress0/uflra/neq-deltacomp.smt + regress0/uflra/pb_real_10_0100_10_10.smt + regress0/uflra/pb_real_10_0100_10_11.smt + regress0/uflra/pb_real_10_0100_10_15.smt + regress0/uflra/pb_real_10_0100_10_16.smt + regress0/uflra/pb_real_10_0100_10_19.smt + regress0/uflra/pb_real_10_0200_10_22.smt + regress0/uflra/pb_real_10_0200_10_26.smt + regress0/uflra/pb_real_10_0200_10_29.smt + regress0/uflra/simple.01.cvc + regress0/uflra/simple.02.cvc + regress0/uflra/simple.03.cvc + regress0/uflra/simple.04.cvc + regress0/unconstrained/arith.smt2 + regress0/unconstrained/arith3.smt2 + regress0/unconstrained/arith4.smt2 + regress0/unconstrained/arith5.smt2 + regress0/unconstrained/arith6.smt2 + regress0/unconstrained/array1.smt2 + regress0/unconstrained/bvbool.smt2 + regress0/unconstrained/bvbool2.smt2 + regress0/unconstrained/bvbool3.smt2 + regress0/unconstrained/bvcmp.smt2 + regress0/unconstrained/bvconcat2.smt2 + regress0/unconstrained/bvext.smt2 + regress0/unconstrained/bvite.smt2 + regress0/unconstrained/bvmul.smt2 + regress0/unconstrained/bvmul2.smt2 + regress0/unconstrained/bvmul3.smt2 + regress0/unconstrained/bvnot.smt2 + regress0/unconstrained/bvsle.smt2 + regress0/unconstrained/bvsle2.smt2 + regress0/unconstrained/bvsle3.smt2 + regress0/unconstrained/bvsle4.smt2 + regress0/unconstrained/bvsle5.smt2 + regress0/unconstrained/bvslt.smt2 + regress0/unconstrained/bvslt2.smt2 + regress0/unconstrained/bvslt3.smt2 + regress0/unconstrained/bvslt4.smt2 + regress0/unconstrained/bvslt5.smt2 + regress0/unconstrained/bvule.smt2 + regress0/unconstrained/bvule2.smt2 + regress0/unconstrained/bvule3.smt2 + regress0/unconstrained/bvule4.smt2 + regress0/unconstrained/bvule5.smt2 + regress0/unconstrained/bvult.smt2 + regress0/unconstrained/bvult2.smt2 + regress0/unconstrained/bvult3.smt2 + regress0/unconstrained/bvult4.smt2 + regress0/unconstrained/bvult5.smt2 + regress0/unconstrained/geq.smt2 + regress0/unconstrained/gt.smt2 + regress0/unconstrained/ite.smt2 + regress0/unconstrained/leq.smt2 + regress0/unconstrained/lt.smt2 + regress0/unconstrained/mult1.smt2 + regress0/unconstrained/uf1.smt2 + regress0/unconstrained/xor.smt2 + regress0/wiki.01.cvc + regress0/wiki.02.cvc + regress0/wiki.03.cvc + regress0/wiki.04.cvc + regress0/wiki.05.cvc + regress0/wiki.06.cvc + regress0/wiki.07.cvc + regress0/wiki.08.cvc + regress0/wiki.09.cvc + regress0/wiki.10.cvc + regress0/wiki.11.cvc + regress0/wiki.12.cvc + regress0/wiki.13.cvc + regress0/wiki.14.cvc + regress0/wiki.15.cvc + regress0/wiki.16.cvc + regress0/wiki.17.cvc + regress0/wiki.18.cvc + regress0/wiki.19.cvc + regress0/wiki.20.cvc + regress0/wiki.21.cvc + regress0/bv/ackermann1.smt2 + regress0/bv/ackermann2.smt2 + regress0/datatypes/data-nested-codata.smt2 + regress0/fmf/sort-infer-typed-082718.smt2 + regress0/fp/ext-rew-test.smt2 + regress0/nl/ext-rew-aggr-test.smt2 + regress0/nl/nlExtPurify-test.smt2 + regress0/quantifiers/issue2035.smt2 + regress0/smtlib/get-unsat-assumptions.smt2 + regress0/strings/rewrites-re-concat.smt2 + regress0/strings/str_unsound_ext_rew_eq.smt2 + regress0/sygus/hd-05-d1-prog-nogrammar.sy ) set(regress_1_tests - regress1/arith/arith-int-004.cvc - regress1/arith/arith-int-011.cvc - regress1/arith/arith-int-012.cvc - regress1/arith/arith-int-013.cvc - regress1/arith/arith-int-022.cvc - regress1/arith/arith-int-024.cvc - regress1/arith/arith-int-047.cvc - regress1/arith/arith-int-048.cvc - regress1/arith/arith-int-050.cvc - regress1/arith/arith-int-084.cvc - regress1/arith/arith-int-085.cvc - regress1/arith/arith-int-097.cvc - regress1/arith/bug547.1.smt2 - regress1/arith/bug716.0.smt2 - regress1/arith/bug716.1.cvc - regress1/arith/div.03.smt2 - regress1/arith/div.06.smt2 - regress1/arith/div.08.smt2 - regress1/arith/div.09.smt2 - regress1/arith/miplib3.cvc - regress1/arith/mod.02.smt2 - regress1/arith/mod.03.smt2 - regress1/arith/mult.02.smt2 - regress1/arith/pbrewrites-test.smt2 - regress1/arith/problem__003.smt2 - regress1/arith/real2int-test.smt2 - regress1/arrayinuf_error.smt2 - regress1/aufbv/bug580.smt2 - regress1/aufbv/fuzz10.smt - regress1/auflia/bug330.smt2 - regress1/boolean-terms-kernel2.smt2 - regress1/boolean.cvc - regress1/bug216.smt2 - regress1/bug296.smt2 - regress1/bug425.cvc - regress1/bug507.smt2 - regress1/bug512.smt2 - regress1/bug516.smt2 - regress1/bug519.smt2 - regress1/bug520.smt2 - regress1/bug521.smt2 - regress1/bug543.smt2 - regress1/bug567.smt2 - regress1/bug593.smt2 - regress1/bug681.smt2 - regress1/bug694-Unapply1.scala-0.smt2 - regress1/bug800.smt2 - regress1/bv/bug787.smt2 - regress1/bv/bug_extract_mult_leading_bit.smt2 - regress1/bv/bv-int-collapse2-sat.smt2 - regress1/bv/bv-proof00.smt - regress1/bv/bv2nat-ground.smt2 - regress1/bv/bv2nat-simp-range-sat.smt2 - regress1/bv/bv2nat-types.smt2 - regress1/bv/cmu-rdk-3.smt2 - regress1/bv/decision-weight00.smt2 - regress1/bv/divtest.smt2 - regress1/bv/fuzz34.smt - regress1/bv/fuzz38.smt - regress1/bv/test-bv-abstraction.smt2 - regress1/bv/unsound1.smt2 - regress1/bvdiv2.smt2 - regress1/constarr3.cvc - regress1/constarr3.smt2 - regress1/datatypes/acyclicity-sr-ground096.smt2 - regress1/datatypes/dt-color-2.6.smt2 - regress1/datatypes/dt-param-card4-unsat.smt2 - regress1/datatypes/error.cvc - regress1/datatypes/manos-model.smt2 - regress1/decision/error3.smt - regress1/decision/quant-Arrays_Q1-noinfer.smt2 - regress1/decision/quant-symmetric_unsat_7.smt2 - regress1/error.cvc - regress1/errorcrash.smt2 - regress1/fmf-fun-dbu.smt2 - regress1/fmf/ALG008-1.smt2 - regress1/fmf/Hoare-z3.931718.smt - regress1/fmf/LeftistHeap.scala-8-ncm.smt2 - regress1/fmf/PUZ001+1.smt2 - regress1/fmf/agree466.smt2 - regress1/fmf/agree467.smt2 - regress1/fmf/alg202+1.smt2 - regress1/fmf/am-bad-model.cvc - regress1/fmf/bound-int-alt.smt2 - regress1/fmf/bug0909.smt2 - regress1/fmf/bug651.smt2 - regress1/fmf/bug723-irrelevant-funs.smt2 - regress1/fmf/bug764.smt2 - regress1/fmf/cons-sets-bounds.smt2 - regress1/fmf/constr-ground-to.smt2 - regress1/fmf/datatypes-ufinite-nested.smt2 - regress1/fmf/datatypes-ufinite.smt2 - regress1/fmf/dt-proper-model.smt2 - regress1/fmf/fc-pigeonhole19.smt2 - regress1/fmf/fib-core.smt2 - regress1/fmf/fmf-bound-2dim.smt2 - regress1/fmf/fmf-bound-int.smt2 - regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 - regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 - regress1/fmf/fmf-strange-bounds.smt2 - regress1/fmf/forall_unit_data.smt2 - regress1/fmf/fore19-exp2-core.smt2 - regress1/fmf/german169.smt2 - regress1/fmf/german73.smt2 - regress1/fmf/issue916-fmf-or.smt2 - regress1/fmf/issue2034-preinit.smt2 - regress1/fmf/jasmin-cdt-crash.smt2 - regress1/fmf/ko-bound-set.cvc - regress1/fmf/loopy_coda.smt2 - regress1/fmf/lst-no-self-rev-exp.smt2 - regress1/fmf/memory_model-R_cpp-dd.cvc - regress1/fmf/nlp042+1.smt2 - regress1/fmf/nun-0208-to.smt2 - regress1/fmf/pow2-bool.smt2 - regress1/fmf/radu-quant-set.smt2 - regress1/fmf/refcount24.cvc.smt2 - regress1/fmf/sc-crash-052316.smt2 - regress1/fmf/with-ind-104-core.smt2 - regress1/gensys_brn001.smt2 - regress1/ho/auth0068.smt2 - regress1/ho/fta0210.smt2 - regress1/ho/fta0409.smt2 - regress1/ho/hoa0008.smt2 - regress1/ho/ho-exponential-model.smt2 - regress1/ho/ho-matching-enum-2.smt2 - regress1/ho/ho-std-fmf.smt2 - regress1/ho/match-middle.smt2 - regress1/hole6.cvc - regress1/ite5.smt2 - regress1/lemmas/clocksynchro_5clocks.main_invar.base.smt - regress1/lemmas/pursuit-safety-8.smt - regress1/lemmas/simple_startup_9nodes.abstract.base.smt - regress1/nl/NAVIGATION2.smt2 - regress1/nl/approx-sqrt.smt2 - regress1/nl/approx-sqrt-unsat.smt2 - regress1/nl/arctan2-expdef.smt2 - regress1/nl/arrowsmith-050317.smt2 - regress1/nl/bad-050217.smt2 - regress1/nl/bug698.smt2 - regress1/nl/coeff-unsat-base.smt2 - regress1/nl/coeff-unsat.smt2 - regress1/nl/combine.smt2 - regress1/nl/cos-bound.smt2 - regress1/nl/cos1-tc.smt2 - regress1/nl/disj-eval.smt2 - regress1/nl/dist-big.smt2 - regress1/nl/div-mod-partial.smt2 - regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 - regress1/nl/exp-4.5-lt.smt2 - regress1/nl/exp1-lb.smt2 - regress1/nl/exp_monotone.smt2 - regress1/nl/factor_agg_s.smt2 - regress1/nl/metitarski-1025.smt2 - regress1/nl/metitarski-3-4.smt2 - regress1/nl/metitarski_3_4_2e.smt2 - regress1/nl/mirko-050417.smt2 - regress1/nl/nl-eq-infer.smt2 - regress1/nl/nl-help-unsat-quant.smt2 - regress1/nl/nl-unk-quant.smt2 - regress1/nl/nl_uf_lalt.smt2 - regress1/nl/ones.smt2 - regress1/nl/poly-1025.smt2 - regress1/nl/quant-nl.smt2 - regress1/nl/red-exp.smt2 - regress1/nl/rewriting-sums.smt2 - regress1/nl/shifting.smt2 - regress1/nl/shifting2.smt2 - regress1/nl/simple-mono-unsat.smt2 - regress1/nl/simple-mono.smt2 - regress1/nl/sin-compare-across-phase.smt2 - regress1/nl/sin-compare.smt2 - regress1/nl/sin-init-tangents.smt2 - regress1/nl/sin-sign.smt2 - regress1/nl/sin-sym2.smt2 - regress1/nl/sin1-deq-sat.smt2 - regress1/nl/sin1-lb.smt2 - regress1/nl/sin1-sat.smt2 - regress1/nl/sin1-ub.smt2 - regress1/nl/sin2-lb.smt2 - regress1/nl/sin2-ub.smt2 - regress1/nl/solve-eq-small-qf-nra.smt2 - regress1/nl/sqrt-problem-1.smt2 - regress1/nl/sugar-ident-2.smt2 - regress1/nl/sugar-ident-3.smt2 - regress1/nl/sugar-ident.smt2 - regress1/nl/tan-rewrite2.smt2 - regress1/nl/zero-subset.smt2 - regress1/non-fatal-errors.smt2 - regress1/parsing_ringer.cvc - regress1/proof00.smt2 - regress1/push-pop/arith_lra_01.smt2 - regress1/push-pop/arith_lra_02.smt2 - regress1/push-pop/bug-fmf-fun-skolem.smt2 - regress1/push-pop/bug216.smt2 - regress1/push-pop/bug326.smt2 - regress1/push-pop/fuzz_1.smt2 - regress1/push-pop/fuzz_10.smt2 - regress1/push-pop/fuzz_11.smt2 - regress1/push-pop/fuzz_15.smt2 - regress1/push-pop/fuzz_16.smt2 - regress1/push-pop/fuzz_19.smt2 - regress1/push-pop/fuzz_1_to_52_merged.smt2 - regress1/push-pop/fuzz_20.smt2 - regress1/push-pop/fuzz_23.smt2 - regress1/push-pop/fuzz_24.smt2 - regress1/push-pop/fuzz_25.smt2 - regress1/push-pop/fuzz_26.smt2 - regress1/push-pop/fuzz_28.smt2 - regress1/push-pop/fuzz_29.smt2 - regress1/push-pop/fuzz_30.smt2 - regress1/push-pop/fuzz_32.smt2 - regress1/push-pop/fuzz_34.smt2 - regress1/push-pop/fuzz_35.smt2 - regress1/push-pop/fuzz_37.smt2 - regress1/push-pop/fuzz_39.smt2 - regress1/push-pop/fuzz_3_1.smt2 - regress1/push-pop/fuzz_3_10.smt2 - regress1/push-pop/fuzz_3_11.smt2 - regress1/push-pop/fuzz_3_12.smt2 - regress1/push-pop/fuzz_3_13.smt2 - regress1/push-pop/fuzz_3_14.smt2 - regress1/push-pop/fuzz_3_15.smt2 - regress1/push-pop/fuzz_3_2.smt2 - regress1/push-pop/fuzz_3_3.smt2 - regress1/push-pop/fuzz_3_4.smt2 - regress1/push-pop/fuzz_3_5.smt2 - regress1/push-pop/fuzz_3_6.smt2 - regress1/push-pop/fuzz_3_7.smt2 - regress1/push-pop/fuzz_3_8.smt2 - regress1/push-pop/fuzz_3_9.smt2 - regress1/push-pop/fuzz_4.smt2 - regress1/push-pop/fuzz_40.smt2 - regress1/push-pop/fuzz_41.smt2 - regress1/push-pop/fuzz_42.smt2 - regress1/push-pop/fuzz_43.smt2 - regress1/push-pop/fuzz_44.smt2 - regress1/push-pop/fuzz_45.smt2 - regress1/push-pop/fuzz_5.smt2 - regress1/push-pop/fuzz_51.smt2 - regress1/push-pop/fuzz_52.smt2 - regress1/push-pop/fuzz_5_1.smt2 - regress1/push-pop/fuzz_5_2.smt2 - regress1/push-pop/fuzz_5_3.smt2 - regress1/push-pop/fuzz_5_4.smt2 - regress1/push-pop/fuzz_5_5.smt2 - regress1/push-pop/fuzz_5_6.smt2 - regress1/push-pop/fuzz_6.smt2 - regress1/push-pop/fuzz_7.smt2 - regress1/push-pop/fuzz_8.smt2 - regress1/push-pop/fuzz_9.smt2 - regress1/push-pop/quant-fun-proc-unmacro.smt2 - regress1/push-pop/quant-fun-proc.smt2 - regress1/quantifiers/006-cbqi-ite.smt2 - regress1/quantifiers/015-psyco-pp.smt2 - regress1/quantifiers/AdditiveMethods_OwnedResults.Mz.smt2 - regress1/quantifiers/Arrays_Q1-noinfer.smt2 - regress1/quantifiers/NUM878.smt2 - regress1/quantifiers/RND-small.smt2 - regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2 - regress1/quantifiers/RND_4_1-existing-inst.smt2 - regress1/quantifiers/RND_4_16.smt2 - regress1/quantifiers/anti-sk-simp.smt2 - regress1/quantifiers/ari118-bv-2occ-x.smt2 - regress1/quantifiers/arith-rec-fun.smt2 - regress1/quantifiers/array-unsat-simp3.smt2 - regress1/quantifiers/bi-artm-s.smt2 - regress1/quantifiers/bignum_quant.smt2 - regress1/quantifiers/bug802.smt2 - regress1/quantifiers/bug822.smt2 - regress1/quantifiers/bug_743.smt2 - regress1/quantifiers/burns13.smt2 - regress1/quantifiers/burns4.smt2 - regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 - regress1/quantifiers/cdt-0208-to.smt2 - regress1/quantifiers/const.cvc - regress1/quantifiers/constfunc.cvc - regress1/quantifiers/ext-ex-deq-trigger.smt2 - regress1/quantifiers/extract-nproc.smt2 - regress1/quantifiers/florian-case-ax.smt2 - regress1/quantifiers/fp-cegqi-unsat.smt2 - regress1/quantifiers/gauss_init_0030.fof.smt2 - regress1/quantifiers/horn-simple.smt2 - regress1/quantifiers/inst-max-level-segf.smt2 - regress1/quantifiers/inst-prop-simp.smt2 - regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 - regress1/quantifiers/isaplanner-goal20.smt2 - regress1/quantifiers/is-even.smt2 - regress1/quantifiers/javafe.ast.StmtVec.009.smt2 - regress1/quantifiers/mix-coeff.smt2 - regress1/quantifiers/model_6_1_bv.smt2 - regress1/quantifiers/mutualrec2.cvc - regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 - regress1/quantifiers/nra-interleave-inst.smt2 - regress1/quantifiers/opisavailable-12.smt2 - regress1/quantifiers/parametric-lists.smt2 - regress1/quantifiers/psyco-001-bv.smt2 - regress1/quantifiers/psyco-107-bv.smt2 - regress1/quantifiers/psyco-196.smt2 - regress1/quantifiers/qbv-disequality3.smt2 - regress1/quantifiers/qbv-simple-2vars-vo.smt2 - regress1/quantifiers/qbv-subcall.smt2 - regress1/quantifiers/qbv-test-invert-bvashr-0.smt2 - regress1/quantifiers/qbv-test-invert-bvashr-1.smt2 - regress1/quantifiers/qbv-test-invert-bvcomp.smt2 - regress1/quantifiers/qbv-test-invert-bvlshr-1.smt2 - regress1/quantifiers/qbv-test-invert-bvmul-neq.smt2 - regress1/quantifiers/qbv-test-invert-bvmul.smt2 - regress1/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2 - regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2 - regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 - regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 - regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 - regress1/quantifiers/qbv-test-invert-bvurem-1.smt2 - regress1/quantifiers/qbv-test-urem-rewrite.smt2 - regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 - regress1/quantifiers/qcft-smtlib3dbc51.smt2 - regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 - regress1/quantifiers/repair-const-nterm.smt2 - regress1/quantifiers/recfact.cvc - regress1/quantifiers/rew-to-0211-dd.smt2 - regress1/quantifiers/ricart-agrawala6.smt2 - regress1/quantifiers/set8.smt2 - regress1/quantifiers/set-choice-koikonomou.cvc - regress1/quantifiers/small-pipeline-fixpoint-3.smt2 - regress1/quantifiers/smtcomp-qbv-053118.smt2 - regress1/quantifiers/smtlib384a03.smt2 - regress1/quantifiers/smtlib46f14a.smt2 - regress1/quantifiers/smtlibe99bbe.smt2 - regress1/quantifiers/smtlibf957ea.smt2 - regress1/quantifiers/stream-x2014-09-18-unsat.smt2 - regress1/quantifiers/sygus-infer-nested.smt2 - regress1/quantifiers/symmetric_unsat_7.smt2 - regress1/quantifiers/z3.620661-no-fv-trigger.smt2 - regress1/rels/addr_book_1.cvc - regress1/rels/addr_book_1_1.cvc - regress1/rels/bv1-unit.cvc - regress1/rels/bv1-unitb.cvc - regress1/rels/bv1.cvc - regress1/rels/bv1p-sat.cvc - regress1/rels/bv1p.cvc - regress1/rels/bv2.cvc - regress1/rels/iden_1_1.cvc - regress1/rels/join-eq-structure-and.cvc - regress1/rels/join-eq-structure.cvc - regress1/rels/join-eq-structure_0_1.cvc - regress1/rels/joinImg_0_1.cvc - regress1/rels/joinImg_0_2.cvc - regress1/rels/joinImg_1.cvc - regress1/rels/joinImg_1_1.cvc - regress1/rels/joinImg_2.cvc - regress1/rels/joinImg_2_1.cvc - regress1/rels/prod-mod-eq.cvc - regress1/rels/prod-mod-eq2.cvc - regress1/rels/rel_complex_3.cvc - regress1/rels/rel_complex_4.cvc - regress1/rels/rel_complex_5.cvc - regress1/rels/rel_mix_0_1.cvc - regress1/rels/rel_pressure_0.cvc - regress1/rels/rel_tc_10_1.cvc - regress1/rels/rel_tc_4.cvc - regress1/rels/rel_tc_4_1.cvc - regress1/rels/rel_tc_5_1.cvc - regress1/rels/rel_tc_6.cvc - regress1/rels/rel_tc_9_1.cvc - regress1/rels/rel_tp_2.cvc - regress1/rels/rel_tp_join_2_1.cvc - regress1/rels/set-strat.cvc - regress1/rels/strat.cvc - regress1/rels/strat_0_1.cvc - regress1/rewriterules/datatypes_sat.smt2 - regress1/rewriterules/length_gen.smt2 - regress1/rewriterules/length_gen_020.smt2 - regress1/rewriterules/length_gen_020_sat.smt2 - regress1/rewriterules/length_gen_040.smt2 - regress1/rewriterules/length_gen_040_lemma.smt2 - regress1/rewriterules/length_gen_040_lemma_trigger.smt2 - regress1/rewriterules/reachability_back_to_the_future.smt2 - regress1/rewriterules/read5.smt2 - regress1/sep/chain-int.smt2 - regress1/sep/crash1220.smt2 - regress1/sep/dispose-list-4-init.smt2 - regress1/sep/emp2-quant-unsat.smt2 - regress1/sep/finite-witness-sat.smt2 - regress1/sep/fmf-nemp-2.smt2 - regress1/sep/loop-1220.smt2 - regress1/sep/pto-04.smt2 - regress1/sep/quant_wand.smt2 - regress1/sep/sep-02.smt2 - regress1/sep/sep-03.smt2 - regress1/sep/sep-find2.smt2 - regress1/sep/sep-fmf-priority.smt2 - regress1/sep/sep-neg-1refine.smt2 - regress1/sep/sep-neg-nstrict.smt2 - regress1/sep/sep-neg-nstrict2.smt2 - regress1/sep/sep-neg-simple.smt2 - regress1/sep/sep-neg-swap.smt2 - regress1/sep/sep-nterm-again.smt2 - regress1/sep/sep-nterm-val-model.smt2 - regress1/sep/sep-simp-unc.smt2 - regress1/sep/simple-neg-sat.smt2 - regress1/sep/sl-standard.smt2 - regress1/sep/split-find-unsat-w-emp.smt2 - regress1/sep/split-find-unsat.smt2 - regress1/sep/wand-0526-sat.smt2 - regress1/sep/wand-false.smt2 - regress1/sep/wand-nterm-simp.smt2 - regress1/sep/wand-nterm-simp2.smt2 - regress1/sep/wand-simp-sat.smt2 - regress1/sep/wand-simp-sat2.smt2 - regress1/sep/wand-simp-unsat.smt2 - regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 - regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 - regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 - regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 - regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 - regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 - regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 - regress1/sets/arjun-set-univ.cvc - regress1/sets/card-3.smt2 - regress1/sets/card-4.smt2 - regress1/sets/card-5.smt2 - regress1/sets/card-6.smt2 - regress1/sets/card-7.smt2 - regress1/sets/card-vc6-minimized.smt2 - regress1/sets/copy_check_heap_access_33_4.smt2 - regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 - regress1/sets/fuzz14418.smt2 - regress1/sets/fuzz15201.smt2 - regress1/sets/fuzz31811.smt2 - regress1/sets/insert_invariant_37_2.smt2 - regress1/sets/lemmabug-ListElts317minimized.smt2 - regress1/sets/remove_check_free_31_6.smt2 - regress1/sets/sets-disequal.smt2 - regress1/sets/sets-tuple-poly.cvc - regress1/sets/sharingbug.smt2 - regress1/sets/univ-set-uf-elim.smt2 - regress1/simplification_bug4.smt2 - regress1/sqrt2-sort-inf-unk.smt2 - regress1/strings/artemis-0512-nonterm.smt2 - regress1/strings/at001.smt2 - regress1/strings/bug615.smt2 - regress1/strings/bug682.smt2 - regress1/strings/bug686dd.smt2 - regress1/strings/bug768.smt2 - regress1/strings/bug799-min.smt2 - regress1/strings/chapman150408.smt2 - regress1/strings/cmu-2db2-extf-reg.smt2 - regress1/strings/cmu-5042-0707-2.smt2 - regress1/strings/cmu-inc-nlpp-071516.smt2 - regress1/strings/cmu-substr-rw.smt2 - regress1/strings/code-sequence.smt2 - regress1/strings/crash-1019.smt2 - regress1/strings/csp-prefix-exp-bug.smt2 - regress1/strings/double-replace.smt2 - regress1/strings/fmf001.smt2 - regress1/strings/fmf002.smt2 - regress1/strings/gm-inc-071516-2.smt2 - regress1/strings/goodAI.smt2 - regress1/strings/idof-handg.smt2 - regress1/strings/idof-nconst-index.smt2 - regress1/strings/idof-neg-index.smt2 - regress1/strings/idof-triv.smt2 - regress1/strings/ilc-l-nt.smt2 - regress1/strings/issue1105.smt2 - regress1/strings/issue2060.smt2 - regress1/strings/kaluza-fl.smt2 - regress1/strings/loop002.smt2 - regress1/strings/loop003.smt2 - regress1/strings/loop004.smt2 - regress1/strings/loop005.smt2 - regress1/strings/loop006.smt2 - regress1/strings/loop007.smt2 - regress1/strings/loop008.smt2 - regress1/strings/loop009.smt2 - regress1/strings/nf-ff-contains-abs.smt2 - regress1/strings/norn-360.smt2 - regress1/strings/norn-ab.smt2 - regress1/strings/norn-nel-bug-052116.smt2 - regress1/strings/norn-simp-rew-sat.smt2 - regress1/strings/nterm-re-inter-sigma.smt2 - regress1/strings/pierre150331.smt2 - regress1/strings/re-unsound-080718.smt2 - regress1/strings/regexp001.smt2 - regress1/strings/regexp002.smt2 - regress1/strings/regexp003.smt2 - regress1/strings/reloop.smt2 - regress1/strings/repl-empty-sem.smt2 - regress1/strings/repl-soundness-sem.smt2 - regress1/strings/rew-020618.smt2 - regress1/strings/str001.smt2 - regress1/strings/str002.smt2 - regress1/strings/str006.smt2 - regress1/strings/str007.smt2 - regress1/strings/string-unsound-sem.smt2 - regress1/strings/strings-index-empty.smt2 - regress1/strings/strings-leq-trans-unsat.smt2 - regress1/strings/strings-lt-len5.smt2 - regress1/strings/strings-lt-simple.smt2 - regress1/strings/strip-endpt-sound.smt2 - regress1/strings/str-code-sat.smt2 - regress1/strings/str-code-unsat.smt2 - regress1/strings/str-code-unsat-2.smt2 - regress1/strings/str-code-unsat-3.smt2 - regress1/strings/substr001.smt2 - regress1/strings/type002.smt2 - regress1/strings/type003.smt2 - regress1/strings/username_checker_min.smt2 - regress1/sygus/VC22_a.sy - regress1/sygus/array_search_2.sy - regress1/sygus/array_search_5-Q-easy.sy - regress1/sygus/array_sum_2_5.sy - regress1/sygus/cegar1.sy - regress1/sygus/cegisunif-depth1.sy - regress1/sygus/cegis-unif-inv-eq-fair.sy - regress1/sygus/cggmp.sy - regress1/sygus/clock-inc-tuple.sy - regress1/sygus/commutative.sy - regress1/sygus/constant.sy - regress1/sygus/constant-bool-si-all.sy - regress1/sygus/constant-dec-tree-bug.sy - regress1/sygus/constant-ite-bv.sy - regress1/sygus/crci-ssb-unk.sy - regress1/sygus/crcy-si-rcons.sy - regress1/sygus/crcy-si.sy - regress1/sygus/dt-test-ns.sy - regress1/sygus/dup-op.sy - regress1/sygus/fg_polynomial3.sy - regress1/sygus/find_sc_bvult_bvnot.sy - regress1/sygus/hd-01-d1-prog.sy - regress1/sygus/hd-19-d1-prog-dup-op.sy - regress1/sygus/hd-sdiv.sy - regress1/sygus/icfp_14.12-flip-args.sy - regress1/sygus/icfp_14.12.sy - regress1/sygus/icfp_14_12_diff_types.sy - regress1/sygus/icfp_28_10.sy - regress1/sygus/icfp_easy-ite.sy - regress1/sygus/inv-example.sy - regress1/sygus/inv-unused.sy - regress1/sygus/large-const-simp.sy - regress1/sygus/list-head-x.sy - regress1/sygus/logiccell_help.sy - regress1/sygus/max.sy - regress1/sygus/multi-fun-polynomial2.sy - regress1/sygus/nflat-fwd-3.sy - regress1/sygus/nflat-fwd.sy - regress1/sygus/nia-max-square-ns.sy - regress1/sygus/no-flat-simp.sy - regress1/sygus/no-mention.sy - regress1/sygus/parity-si-rcons.sy - regress1/sygus/pbe_multi.sy - regress1/sygus/planning-unif.sy - regress1/sygus/process-10-vars.sy - regress1/sygus/qe.sy - regress1/sygus/real-grammar.sy - regress1/sygus/simple-regexp.sy - regress1/sygus/stopwatch-bt.sy - regress1/sygus/strings-concat-3-args.sy - regress1/sygus/strings-double-rec.sy - regress1/sygus/strings-small.sy - regress1/sygus/strings-template-infer-unused.sy - regress1/sygus/strings-template-infer.sy - regress1/sygus/strings-trivial-simp.sy - regress1/sygus/strings-trivial-two-type.sy - regress1/sygus/strings-trivial.sy - regress1/sygus/sygus-dt.sy - regress1/sygus/sygus-lambda-fv.sy - regress1/sygus/sygus-uf-ex.sy - regress1/sygus/t8.sy - regress1/sygus/tl-type-0.sy - regress1/sygus/tl-type-4x.sy - regress1/sygus/tl-type.sy - regress1/sygus/triv-type-mismatch-si.sy - regress1/sygus/twolets1.sy - regress1/sygus/twolets2-orig.sy - regress1/sygus/unbdd_inv_gen_ex7.sy - regress1/sygus/unbdd_inv_gen_winf1.sy - regress1/sygus/univ_2-long-repeat.sy - regress1/sym/sym1.smt2 - regress1/sym/sym2.smt2 - regress1/sym/sym3.smt2 - regress1/sym/sym4.smt2 - regress1/sym/sym5.smt2 - regress1/sym/sym6.smt2 - regress1/sym/sym7-uf.smt2 - regress1/test12.cvc - regress1/trim.cvc - regress1/uf2.smt2 - regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2 - regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2 - regress1/uflia/FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2 - regress1/uflia/microwave21.ec.minimized.smt2 - regress1/uflia/simple_cyclic2.smt2 - regress1/uflia/speed2_e8_449_e8_517.ec.smt2 - regress1/uflia/stalmark_e7_27_e7_31.ec.smt2 - regress1/wrong-qfabvfp-smtcomp2018.smt2 + regress1/arith/arith-int-004.cvc + regress1/arith/arith-int-011.cvc + regress1/arith/arith-int-012.cvc + regress1/arith/arith-int-013.cvc + regress1/arith/arith-int-022.cvc + regress1/arith/arith-int-024.cvc + regress1/arith/arith-int-047.cvc + regress1/arith/arith-int-048.cvc + regress1/arith/arith-int-050.cvc + regress1/arith/arith-int-084.cvc + regress1/arith/arith-int-085.cvc + regress1/arith/arith-int-097.cvc + regress1/arith/bug547.1.smt2 + regress1/arith/bug716.0.smt2 + regress1/arith/bug716.1.cvc + regress1/arith/div.03.smt2 + regress1/arith/div.06.smt2 + regress1/arith/div.08.smt2 + regress1/arith/div.09.smt2 + regress1/arith/miplib3.cvc + regress1/arith/mod.02.smt2 + regress1/arith/mod.03.smt2 + regress1/arith/mult.02.smt2 + regress1/arith/pbrewrites-test.smt2 + regress1/arith/problem__003.smt2 + regress1/arith/real2int-test.smt2 + regress1/arrayinuf_error.smt2 + regress1/aufbv/bug580.smt2 + regress1/aufbv/fuzz10.smt + regress1/auflia/bug330.smt2 + regress1/boolean-terms-kernel2.smt2 + regress1/boolean.cvc + regress1/bug216.smt2 + regress1/bug296.smt2 + regress1/bug425.cvc + regress1/bug507.smt2 + regress1/bug512.smt2 + regress1/bug516.smt2 + regress1/bug519.smt2 + regress1/bug520.smt2 + regress1/bug521.smt2 + regress1/bug543.smt2 + regress1/bug567.smt2 + regress1/bug593.smt2 + regress1/bug681.smt2 + regress1/bug694-Unapply1.scala-0.smt2 + regress1/bug800.smt2 + regress1/bv/bug787.smt2 + regress1/bv/bug_extract_mult_leading_bit.smt2 + regress1/bv/bv-int-collapse2-sat.smt2 + regress1/bv/bv-proof00.smt + regress1/bv/bv2nat-ground.smt2 + regress1/bv/bv2nat-simp-range-sat.smt2 + regress1/bv/bv2nat-types.smt2 + regress1/bv/cmu-rdk-3.smt2 + regress1/bv/decision-weight00.smt2 + regress1/bv/divtest.smt2 + regress1/bv/fuzz34.smt + regress1/bv/fuzz38.smt + regress1/bv/test-bv-abstraction.smt2 + regress1/bv/unsound1.smt2 + regress1/bvdiv2.smt2 + regress1/constarr3.cvc + regress1/constarr3.smt2 + regress1/datatypes/acyclicity-sr-ground096.smt2 + regress1/datatypes/dt-color-2.6.smt2 + regress1/datatypes/dt-param-card4-unsat.smt2 + regress1/datatypes/error.cvc + regress1/datatypes/manos-model.smt2 + regress1/decision/error3.smt + regress1/decision/quant-Arrays_Q1-noinfer.smt2 + regress1/decision/quant-symmetric_unsat_7.smt2 + regress1/error.cvc + regress1/errorcrash.smt2 + regress1/fmf-fun-dbu.smt2 + regress1/fmf/ALG008-1.smt2 + regress1/fmf/Hoare-z3.931718.smt + regress1/fmf/LeftistHeap.scala-8-ncm.smt2 + regress1/fmf/PUZ001+1.smt2 + regress1/fmf/agree466.smt2 + regress1/fmf/agree467.smt2 + regress1/fmf/alg202+1.smt2 + regress1/fmf/am-bad-model.cvc + regress1/fmf/bound-int-alt.smt2 + regress1/fmf/bug0909.smt2 + regress1/fmf/bug651.smt2 + regress1/fmf/bug723-irrelevant-funs.smt2 + regress1/fmf/bug764.smt2 + regress1/fmf/cons-sets-bounds.smt2 + regress1/fmf/constr-ground-to.smt2 + regress1/fmf/datatypes-ufinite-nested.smt2 + regress1/fmf/datatypes-ufinite.smt2 + regress1/fmf/dt-proper-model.smt2 + regress1/fmf/fc-pigeonhole19.smt2 + regress1/fmf/fib-core.smt2 + regress1/fmf/fmf-bound-2dim.smt2 + regress1/fmf/fmf-bound-int.smt2 + regress1/fmf/fmf-fun-divisor-pp.smt2 + regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 + regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 + regress1/fmf/fmf-strange-bounds.smt2 + regress1/fmf/forall_unit_data.smt2 + regress1/fmf/fore19-exp2-core.smt2 + regress1/fmf/german169.smt2 + regress1/fmf/german73.smt2 + regress1/fmf/issue2034-preinit.smt2 + regress1/fmf/issue916-fmf-or.smt2 + regress1/fmf/jasmin-cdt-crash.smt2 + regress1/fmf/ko-bound-set.cvc + regress1/fmf/loopy_coda.smt2 + regress1/fmf/lst-no-self-rev-exp.smt2 + regress1/fmf/memory_model-R_cpp-dd.cvc + regress1/fmf/nlp042+1.smt2 + regress1/fmf/nun-0208-to.smt2 + regress1/fmf/pow2-bool.smt2 + regress1/fmf/radu-quant-set.smt2 + regress1/fmf/refcount24.cvc.smt2 + regress1/fmf/sc-crash-052316.smt2 + regress1/fmf/sort-inf-int-real.smt2 + regress1/fmf/sort-inf-int.smt2 + regress1/fmf/with-ind-104-core.smt2 + regress1/gensys_brn001.smt2 + regress1/ho/auth0068.smt2 + regress1/ho/fta0210.smt2 + regress1/ho/fta0409.smt2 + regress1/ho/ho-exponential-model.smt2 + regress1/ho/ho-matching-enum-2.smt2 + regress1/ho/ho-std-fmf.smt2 + regress1/ho/hoa0008.smt2 + regress1/ho/match-middle.smt2 + regress1/hole6.cvc + regress1/ite5.smt2 + regress1/lemmas/clocksynchro_5clocks.main_invar.base.smt + regress1/lemmas/pursuit-safety-8.smt + regress1/lemmas/simple_startup_9nodes.abstract.base.smt + regress1/nl/NAVIGATION2.smt2 + regress1/nl/approx-sqrt-unsat.smt2 + regress1/nl/approx-sqrt.smt2 + regress1/nl/arctan2-expdef.smt2 + regress1/nl/arrowsmith-050317.smt2 + regress1/nl/bad-050217.smt2 + regress1/nl/bug698.smt2 + regress1/nl/coeff-unsat-base.smt2 + regress1/nl/coeff-unsat.smt2 + regress1/nl/combine.smt2 + regress1/nl/cos-bound.smt2 + regress1/nl/cos1-tc.smt2 + regress1/nl/disj-eval.smt2 + regress1/nl/dist-big.smt2 + regress1/nl/div-mod-partial.smt2 + regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 + regress1/nl/exp-4.5-lt.smt2 + regress1/nl/exp1-lb.smt2 + regress1/nl/exp_monotone.smt2 + regress1/nl/factor_agg_s.smt2 + regress1/nl/metitarski-1025.smt2 + regress1/nl/metitarski-3-4.smt2 + regress1/nl/metitarski_3_4_2e.smt2 + regress1/nl/mirko-050417.smt2 + regress1/nl/nl-eq-infer.smt2 + regress1/nl/nl-help-unsat-quant.smt2 + regress1/nl/nl-unk-quant.smt2 + regress1/nl/nl_uf_lalt.smt2 + regress1/nl/ones.smt2 + regress1/nl/poly-1025.smt2 + regress1/nl/quant-nl.smt2 + regress1/nl/red-exp.smt2 + regress1/nl/rewriting-sums.smt2 + regress1/nl/shifting.smt2 + regress1/nl/shifting2.smt2 + regress1/nl/simple-mono-unsat.smt2 + regress1/nl/simple-mono.smt2 + regress1/nl/sin-compare-across-phase.smt2 + regress1/nl/sin-compare.smt2 + regress1/nl/sin-init-tangents.smt2 + regress1/nl/sin-sign.smt2 + regress1/nl/sin-sym2.smt2 + regress1/nl/sin1-deq-sat.smt2 + regress1/nl/sin1-lb.smt2 + regress1/nl/sin1-sat.smt2 + regress1/nl/sin1-ub.smt2 + regress1/nl/sin2-lb.smt2 + regress1/nl/sin2-ub.smt2 + regress1/nl/solve-eq-small-qf-nra.smt2 + regress1/nl/sqrt-problem-1.smt2 + regress1/nl/sugar-ident-2.smt2 + regress1/nl/sugar-ident-3.smt2 + regress1/nl/sugar-ident.smt2 + regress1/nl/tan-rewrite2.smt2 + regress1/nl/zero-subset.smt2 + regress1/non-fatal-errors.smt2 + regress1/parsing_ringer.cvc + regress1/proof00.smt2 + regress1/push-pop/arith_lra_01.smt2 + regress1/push-pop/arith_lra_02.smt2 + regress1/push-pop/bug-fmf-fun-skolem.smt2 + regress1/push-pop/bug216.smt2 + regress1/push-pop/bug326.smt2 + regress1/push-pop/fuzz_1.smt2 + regress1/push-pop/fuzz_10.smt2 + regress1/push-pop/fuzz_11.smt2 + regress1/push-pop/fuzz_15.smt2 + regress1/push-pop/fuzz_16.smt2 + regress1/push-pop/fuzz_19.smt2 + regress1/push-pop/fuzz_1_to_52_merged.smt2 + regress1/push-pop/fuzz_20.smt2 + regress1/push-pop/fuzz_23.smt2 + regress1/push-pop/fuzz_24.smt2 + regress1/push-pop/fuzz_25.smt2 + regress1/push-pop/fuzz_26.smt2 + regress1/push-pop/fuzz_28.smt2 + regress1/push-pop/fuzz_29.smt2 + regress1/push-pop/fuzz_30.smt2 + regress1/push-pop/fuzz_32.smt2 + regress1/push-pop/fuzz_34.smt2 + regress1/push-pop/fuzz_35.smt2 + regress1/push-pop/fuzz_37.smt2 + regress1/push-pop/fuzz_39.smt2 + regress1/push-pop/fuzz_3_1.smt2 + regress1/push-pop/fuzz_3_10.smt2 + regress1/push-pop/fuzz_3_11.smt2 + regress1/push-pop/fuzz_3_12.smt2 + regress1/push-pop/fuzz_3_13.smt2 + regress1/push-pop/fuzz_3_14.smt2 + regress1/push-pop/fuzz_3_15.smt2 + regress1/push-pop/fuzz_3_2.smt2 + regress1/push-pop/fuzz_3_3.smt2 + regress1/push-pop/fuzz_3_4.smt2 + regress1/push-pop/fuzz_3_5.smt2 + regress1/push-pop/fuzz_3_6.smt2 + regress1/push-pop/fuzz_3_7.smt2 + regress1/push-pop/fuzz_3_8.smt2 + regress1/push-pop/fuzz_3_9.smt2 + regress1/push-pop/fuzz_4.smt2 + regress1/push-pop/fuzz_40.smt2 + regress1/push-pop/fuzz_41.smt2 + regress1/push-pop/fuzz_42.smt2 + regress1/push-pop/fuzz_43.smt2 + regress1/push-pop/fuzz_44.smt2 + regress1/push-pop/fuzz_45.smt2 + regress1/push-pop/fuzz_5.smt2 + regress1/push-pop/fuzz_51.smt2 + regress1/push-pop/fuzz_52.smt2 + regress1/push-pop/fuzz_5_1.smt2 + regress1/push-pop/fuzz_5_2.smt2 + regress1/push-pop/fuzz_5_3.smt2 + regress1/push-pop/fuzz_5_4.smt2 + regress1/push-pop/fuzz_5_5.smt2 + regress1/push-pop/fuzz_5_6.smt2 + regress1/push-pop/fuzz_6.smt2 + regress1/push-pop/fuzz_7.smt2 + regress1/push-pop/fuzz_8.smt2 + regress1/push-pop/fuzz_9.smt2 + regress1/push-pop/quant-fun-proc-unmacro.smt2 + regress1/push-pop/quant-fun-proc.smt2 + regress1/quantifiers/006-cbqi-ite.smt2 + regress1/quantifiers/015-psyco-pp.smt2 + regress1/quantifiers/AdditiveMethods_OwnedResults.Mz.smt2 + regress1/quantifiers/Arrays_Q1-noinfer.smt2 + regress1/quantifiers/NUM878.smt2 + regress1/quantifiers/RND-small.smt2 + regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2 + regress1/quantifiers/RND_4_1-existing-inst.smt2 + regress1/quantifiers/RND_4_16.smt2 + regress1/quantifiers/anti-sk-simp.smt2 + regress1/quantifiers/ari118-bv-2occ-x.smt2 + regress1/quantifiers/arith-rec-fun.smt2 + regress1/quantifiers/arith-snorm.smt2 + regress1/quantifiers/array-unsat-simp3.smt2 + regress1/quantifiers/bi-artm-s.smt2 + regress1/quantifiers/bignum_quant.smt2 + regress1/quantifiers/bug802.smt2 + regress1/quantifiers/bug822.smt2 + regress1/quantifiers/bug_743.smt2 + regress1/quantifiers/burns13.smt2 + regress1/quantifiers/burns4.smt2 + regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 + regress1/quantifiers/cdt-0208-to.smt2 + regress1/quantifiers/const.cvc + regress1/quantifiers/constfunc.cvc + regress1/quantifiers/dump-inst-i.smt2 + regress1/quantifiers/dump-inst-proof.smt2 + regress1/quantifiers/dump-inst.smt2 + regress1/quantifiers/ext-ex-deq-trigger.smt2 + regress1/quantifiers/extract-nproc.smt2 + regress1/quantifiers/florian-case-ax.smt2 + regress1/quantifiers/fp-cegqi-unsat.smt2 + regress1/quantifiers/gauss_init_0030.fof.smt2 + regress1/quantifiers/horn-simple.smt2 + regress1/quantifiers/infer-arith-trigger-eq.smt2 + regress1/quantifiers/inst-max-level-segf.smt2 + regress1/quantifiers/inst-prop-simp.smt2 + regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 + regress1/quantifiers/is-even.smt2 + regress1/quantifiers/isaplanner-goal20.smt2 + regress1/quantifiers/javafe.ast.StmtVec.009.smt2 + regress1/quantifiers/lra-vts-inf.smt2 + regress1/quantifiers/mix-coeff.smt2 + regress1/quantifiers/model_6_1_bv.smt2 + regress1/quantifiers/mutualrec2.cvc + regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 + regress1/quantifiers/nl-pow-trick.smt2 + regress1/quantifiers/nra-interleave-inst.smt2 + regress1/quantifiers/opisavailable-12.smt2 + regress1/quantifiers/parametric-lists.smt2 + regress1/quantifiers/psyco-001-bv.smt2 + regress1/quantifiers/psyco-107-bv.smt2 + regress1/quantifiers/psyco-196.smt2 + regress1/quantifiers/qbv-disequality3.smt2 + regress1/quantifiers/qbv-simple-2vars-vo.smt2 + regress1/quantifiers/qbv-subcall.smt2 + regress1/quantifiers/qbv-test-invert-bvashr-0.smt2 + regress1/quantifiers/qbv-test-invert-bvashr-1.smt2 + regress1/quantifiers/qbv-test-invert-bvcomp.smt2 + regress1/quantifiers/qbv-test-invert-bvlshr-1.smt2 + regress1/quantifiers/qbv-test-invert-bvmul-neq.smt2 + regress1/quantifiers/qbv-test-invert-bvmul.smt2 + regress1/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2 + regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2 + regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 + regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 + regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 + regress1/quantifiers/qbv-test-invert-bvurem-1.smt2 + regress1/quantifiers/qbv-test-urem-rewrite.smt2 + regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 + regress1/quantifiers/qcft-smtlib3dbc51.smt2 + regress1/quantifiers/qe-partial.smt2 + regress1/quantifiers/qe.smt2 + regress1/quantifiers/quant-wf-int-ind.smt2 + regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 + regress1/quantifiers/recfact.cvc + regress1/quantifiers/repair-const-nterm.smt2 + regress1/quantifiers/rew-to-0211-dd.smt2 + regress1/quantifiers/ricart-agrawala6.smt2 + regress1/quantifiers/set-choice-koikonomou.cvc + regress1/quantifiers/set8.smt2 + regress1/quantifiers/small-pipeline-fixpoint-3.smt2 + regress1/quantifiers/smtcomp-qbv-053118.smt2 + regress1/quantifiers/smtlib384a03.smt2 + regress1/quantifiers/smtlib46f14a.smt2 + regress1/quantifiers/smtlibe99bbe.smt2 + regress1/quantifiers/smtlibf957ea.smt2 + regress1/quantifiers/stream-x2014-09-18-unsat.smt2 + regress1/quantifiers/sygus-infer-nested.smt2 + regress1/quantifiers/symmetric_unsat_7.smt2 + regress1/quantifiers/z3.620661-no-fv-trigger.smt2 + regress1/rels/addr_book_1.cvc + regress1/rels/addr_book_1_1.cvc + regress1/rels/bv1-unit.cvc + regress1/rels/bv1-unitb.cvc + regress1/rels/bv1.cvc + regress1/rels/bv1p-sat.cvc + regress1/rels/bv1p.cvc + regress1/rels/bv2.cvc + regress1/rels/iden_1_1.cvc + regress1/rels/join-eq-structure-and.cvc + regress1/rels/join-eq-structure.cvc + regress1/rels/join-eq-structure_0_1.cvc + regress1/rels/joinImg_0_1.cvc + regress1/rels/joinImg_0_2.cvc + regress1/rels/joinImg_1.cvc + regress1/rels/joinImg_1_1.cvc + regress1/rels/joinImg_2.cvc + regress1/rels/joinImg_2_1.cvc + regress1/rels/prod-mod-eq.cvc + regress1/rels/prod-mod-eq2.cvc + regress1/rels/rel_complex_3.cvc + regress1/rels/rel_complex_4.cvc + regress1/rels/rel_complex_5.cvc + regress1/rels/rel_mix_0_1.cvc + regress1/rels/rel_pressure_0.cvc + regress1/rels/rel_tc_10_1.cvc + regress1/rels/rel_tc_4.cvc + regress1/rels/rel_tc_4_1.cvc + regress1/rels/rel_tc_5_1.cvc + regress1/rels/rel_tc_6.cvc + regress1/rels/rel_tc_9_1.cvc + regress1/rels/rel_tp_2.cvc + regress1/rels/rel_tp_join_2_1.cvc + regress1/rels/set-strat.cvc + regress1/rels/strat.cvc + regress1/rels/strat_0_1.cvc + regress1/rewriterules/datatypes_sat.smt2 + regress1/rewriterules/length_gen.smt2 + regress1/rewriterules/length_gen_020.smt2 + regress1/rewriterules/length_gen_020_sat.smt2 + regress1/rewriterules/length_gen_040.smt2 + regress1/rewriterules/length_gen_040_lemma.smt2 + regress1/rewriterules/length_gen_040_lemma_trigger.smt2 + regress1/rewriterules/reachability_back_to_the_future.smt2 + regress1/rewriterules/read5.smt2 + regress1/rr-verify/bool-crci.sy + regress1/rr-verify/bv-term-32.sy + regress1/rr-verify/bv-term.sy + regress1/rr-verify/regex.sy + regress1/rr-verify/string-term.sy + regress1/sep/chain-int.smt2 + regress1/sep/crash1220.smt2 + regress1/sep/dispose-list-4-init.smt2 + regress1/sep/emp2-quant-unsat.smt2 + regress1/sep/finite-witness-sat.smt2 + regress1/sep/fmf-nemp-2.smt2 + regress1/sep/loop-1220.smt2 + regress1/sep/pto-04.smt2 + regress1/sep/quant_wand.smt2 + regress1/sep/sep-02.smt2 + regress1/sep/sep-03.smt2 + regress1/sep/sep-find2.smt2 + regress1/sep/sep-fmf-priority.smt2 + regress1/sep/sep-neg-1refine.smt2 + regress1/sep/sep-neg-nstrict.smt2 + regress1/sep/sep-neg-nstrict2.smt2 + regress1/sep/sep-neg-simple.smt2 + regress1/sep/sep-neg-swap.smt2 + regress1/sep/sep-nterm-again.smt2 + regress1/sep/sep-nterm-val-model.smt2 + regress1/sep/sep-simp-unc.smt2 + regress1/sep/simple-neg-sat.smt2 + regress1/sep/sl-standard.smt2 + regress1/sep/split-find-unsat-w-emp.smt2 + regress1/sep/split-find-unsat.smt2 + regress1/sep/wand-0526-sat.smt2 + regress1/sep/wand-false.smt2 + regress1/sep/wand-nterm-simp.smt2 + regress1/sep/wand-nterm-simp2.smt2 + regress1/sep/wand-simp-sat.smt2 + regress1/sep/wand-simp-sat2.smt2 + regress1/sep/wand-simp-unsat.smt2 + regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 + regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 + regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 + regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 + regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 + regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 + regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 + regress1/sets/arjun-set-univ.cvc + regress1/sets/card-3.smt2 + regress1/sets/card-4.smt2 + regress1/sets/card-5.smt2 + regress1/sets/card-6.smt2 + regress1/sets/card-7.smt2 + regress1/sets/card-vc6-minimized.smt2 + regress1/sets/copy_check_heap_access_33_4.smt2 + regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 + regress1/sets/fuzz14418.smt2 + regress1/sets/fuzz15201.smt2 + regress1/sets/fuzz31811.smt2 + regress1/sets/insert_invariant_37_2.smt2 + regress1/sets/lemmabug-ListElts317minimized.smt2 + regress1/sets/remove_check_free_31_6.smt2 + regress1/sets/sets-disequal.smt2 + regress1/sets/sets-tuple-poly.cvc + regress1/sets/sharingbug.smt2 + regress1/sets/univ-set-uf-elim.smt2 + regress1/simplification_bug4.smt2 + regress1/sqrt2-sort-inf-unk.smt2 + regress1/strings/artemis-0512-nonterm.smt2 + regress1/strings/at001.smt2 + regress1/strings/bug615.smt2 + regress1/strings/bug682.smt2 + regress1/strings/bug686dd.smt2 + regress1/strings/bug768.smt2 + regress1/strings/bug799-min.smt2 + regress1/strings/chapman150408.smt2 + regress1/strings/cmu-2db2-extf-reg.smt2 + regress1/strings/cmu-5042-0707-2.smt2 + regress1/strings/cmu-inc-nlpp-071516.smt2 + regress1/strings/cmu-substr-rw.smt2 + regress1/strings/code-sequence.smt2 + regress1/strings/crash-1019.smt2 + regress1/strings/csp-prefix-exp-bug.smt2 + regress1/strings/double-replace.smt2 + regress1/strings/fmf001.smt2 + regress1/strings/fmf002.smt2 + regress1/strings/gm-inc-071516-2.smt2 + regress1/strings/goodAI.smt2 + regress1/strings/idof-handg.smt2 + regress1/strings/idof-nconst-index.smt2 + regress1/strings/idof-neg-index.smt2 + regress1/strings/idof-triv.smt2 + regress1/strings/ilc-l-nt.smt2 + regress1/strings/issue1105.smt2 + regress1/strings/issue1684-regex.smt2 + regress1/strings/issue2060.smt2 + regress1/strings/issue2429-code.smt2 + regress1/strings/kaluza-fl.smt2 + regress1/strings/loop002.smt2 + regress1/strings/loop003.smt2 + regress1/strings/loop004.smt2 + regress1/strings/loop005.smt2 + regress1/strings/loop006.smt2 + regress1/strings/loop007.smt2 + regress1/strings/loop008.smt2 + regress1/strings/loop009.smt2 + regress1/strings/nf-ff-contains-abs.smt2 + regress1/strings/non_termination_regular_expression4.smt2 + regress1/strings/norn-13.smt2 + regress1/strings/norn-360.smt2 + regress1/strings/norn-ab.smt2 + regress1/strings/norn-nel-bug-052116.smt2 + regress1/strings/norn-simp-rew-sat.smt2 + regress1/strings/nterm-re-inter-sigma.smt2 + regress1/strings/pierre150331.smt2 + regress1/strings/policy_variable.smt2 + regress1/strings/re-elim-exact.smt2 + regress1/strings/re-unsound-080718.smt2 + regress1/strings/regexp001.smt2 + regress1/strings/regexp002.smt2 + regress1/strings/regexp003.smt2 + regress1/strings/reloop.smt2 + regress1/strings/repl-empty-sem.smt2 + regress1/strings/repl-soundness-sem.smt2 + regress1/strings/rew-020618.smt2 + regress1/strings/str-code-sat.smt2 + regress1/strings/str-code-unsat-2.smt2 + regress1/strings/str-code-unsat-3.smt2 + regress1/strings/str-code-unsat.smt2 + regress1/strings/str001.smt2 + regress1/strings/str002.smt2 + regress1/strings/str006.smt2 + regress1/strings/str007.smt2 + regress1/strings/string-unsound-sem.smt2 + regress1/strings/strings-index-empty.smt2 + regress1/strings/strings-leq-trans-unsat.smt2 + regress1/strings/strings-lt-len5.smt2 + regress1/strings/strings-lt-simple.smt2 + regress1/strings/strip-endpt-sound.smt2 + regress1/strings/substr001.smt2 + regress1/strings/type002.smt2 + regress1/strings/type003.smt2 + regress1/strings/username_checker_min.smt2 + regress1/sygus/VC22_a.sy + regress1/sygus/abv.sy + regress1/sygus/array_search_2.sy + regress1/sygus/array_search_5-Q-easy.sy + regress1/sygus/array_sum_2_5.sy + regress1/sygus/bvudiv-by-2.sy + regress1/sygus/car_3.lus.sy + regress1/sygus/cegar1.sy + regress1/sygus/cegis-unif-inv-eq-fair.sy + regress1/sygus/cegisunif-depth1.sy + regress1/sygus/cggmp.sy + regress1/sygus/clock-inc-tuple.sy + regress1/sygus/commutative-stream.sy + regress1/sygus/commutative.sy + regress1/sygus/constant-bool-si-all.sy + regress1/sygus/constant-dec-tree-bug.sy + regress1/sygus/constant-ite-bv.sy + regress1/sygus/constant.sy + regress1/sygus/crci-ssb-unk.sy + regress1/sygus/crcy-si-rcons.sy + regress1/sygus/crcy-si.sy + regress1/sygus/dt-test-ns.sy + regress1/sygus/dup-op.sy + regress1/sygus/fg_polynomial3.sy + regress1/sygus/find_sc_bvult_bvnot.sy + regress1/sygus/hd-01-d1-prog.sy + regress1/sygus/hd-19-d1-prog-dup-op.sy + regress1/sygus/hd-sdiv.sy + regress1/sygus/icfp_14.12-flip-args.sy + regress1/sygus/icfp_14.12.sy + regress1/sygus/icfp_14_12_diff_types.sy + regress1/sygus/icfp_28_10.sy + regress1/sygus/icfp_easy-ite.sy + regress1/sygus/inv-example.sy + regress1/sygus/inv-unused.sy + regress1/sygus/large-const-simp.sy + regress1/sygus/let-bug-simp.sy + regress1/sygus/list-head-x.sy + regress1/sygus/logiccell_help.sy + regress1/sygus/max.sy + regress1/sygus/max2-bv.sy + regress1/sygus/multi-fun-polynomial2.sy + regress1/sygus/nflat-fwd-3.sy + regress1/sygus/nflat-fwd.sy + regress1/sygus/nia-max-square-ns.sy + regress1/sygus/no-flat-simp.sy + regress1/sygus/no-mention.sy + regress1/sygus/parity-si-rcons.sy + regress1/sygus/pbe_multi.sy + regress1/sygus/phone-1-long.sy + regress1/sygus/planning-unif.sy + regress1/sygus/process-10-vars.sy + regress1/sygus/qe.sy + regress1/sygus/real-grammar.sy + regress1/sygus/simple-regexp.sy + regress1/sygus/stopwatch-bt.sy + regress1/sygus/strings-concat-3-args.sy + regress1/sygus/strings-double-rec.sy + regress1/sygus/strings-small.sy + regress1/sygus/strings-template-infer-unused.sy + regress1/sygus/strings-template-infer.sy + regress1/sygus/strings-trivial-simp.sy + regress1/sygus/strings-trivial-two-type.sy + regress1/sygus/strings-trivial.sy + regress1/sygus/sygus-dt.sy + regress1/sygus/sygus-lambda-fv.sy + regress1/sygus/sygus-uf-ex.sy + regress1/sygus/t8.sy + regress1/sygus/tl-type-0.sy + regress1/sygus/tl-type-4x.sy + regress1/sygus/tl-type.sy + regress1/sygus/triv-type-mismatch-si.sy + regress1/sygus/trivial-stream.sy + regress1/sygus/twolets1.sy + regress1/sygus/twolets2-orig.sy + regress1/sygus/unbdd_inv_gen_ex7.sy + regress1/sygus/unbdd_inv_gen_winf1.sy + regress1/sygus/univ_2-long-repeat.sy + regress1/sym/q-constant.smt2 + regress1/sym/q-function.smt2 + regress1/sym/qf-function.smt2 + regress1/sym/sb-wrong.smt2 + regress1/sym/sym-setAB.smt2 + regress1/sym/sym1.smt2 + regress1/sym/sym2.smt2 + regress1/sym/sym3.smt2 + regress1/sym/sym4.smt2 + regress1/sym/sym5.smt2 + regress1/sym/sym6.smt2 + regress1/sym/sym7-uf.smt2 + regress1/test12.cvc + regress1/trim.cvc + regress1/uf2.smt2 + regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2 + regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2 + regress1/uflia/FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2 + regress1/uflia/microwave21.ec.minimized.smt2 + regress1/uflia/simple_cyclic2.smt2 + regress1/uflia/speed2_e8_449_e8_517.ec.smt2 + regress1/uflia/stalmark_e7_27_e7_31.ec.smt2 + regress1/wrong-qfabvfp-smtcomp2018.smt2 ) set(regress_2_tests - regress2/DTP_k2_n35_c175_s15.smt2 - regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 - regress2/GEO123+1.minimized.smt2 - regress2/arith/abz5_1400.smt - regress2/arith/lpsat-goal-9.smt2 - regress2/arith/prp-13-24.smt2 - regress2/arith/pursuit-safety-11.smt - regress2/arith/pursuit-safety-12.smt - regress2/arith/qlock-4-10-9.base.cvc.smt2 - regress2/arith/sc-7.base.cvc.smt - regress2/arith/uart-8.base.cvc.smt - regress2/auflia-fuzz06.smt - regress2/bug136.smt - regress2/bug148.smt - regress2/bug394.smt2 - regress2/bug674.smt2 - regress2/bug765.smt2 - regress2/bug812.smt2 - regress2/error0.smt2 - regress2/error1.smt - regress2/friedman_n4_i5.smt - regress2/fuzz_2.smt - regress2/hash_sat_06_19.smt2 - regress2/hash_sat_07_17.smt2 - regress2/hash_sat_09_09.smt2 - regress2/hash_sat_10_09.smt2 - regress2/hole7.cvc - regress2/hole8.cvc - regress2/instance_1444.smt - regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2 - regress2/javafe.ast.WhileStmt.447_no_forall.smt2 - regress2/nl/siegel-nl-bases.smt2 - regress2/ooo.rf6.smt2 - regress2/ooo.tag10.smt2 - regress2/piVC_5581bd.smt2 - regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2 - regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 - regress2/quantifiers/javafe.ast.ArrayInit.35.smt2 - regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 - regress2/quantifiers/javafe.ast.WhileStmt.447.smt2 - regress2/quantifiers/javafe.tc.CheckCompilationUnit.001.smt2 - regress2/quantifiers/javafe.tc.FlowInsensitiveChecks.682.smt2 - regress2/quantifiers/mutualrec2.cvc - regress2/quantifiers/net-policy-no-time.smt2 - regress2/quantifiers/nunchaku2309663.nun.min.smt2 - regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2 - regress2/strings/cmu-dis-0707-3.smt2 - regress2/strings/cmu-disagree-0707-dd.smt2 - regress2/strings/cmu-prereg-fmf.smt2 - regress2/strings/cmu-repl-len-nterm.smt2 - regress2/strings/norn-dis-0707-3.smt2 - regress2/sygus/MPwL_d1s3.sy - regress2/sygus/array_sum_dd.sy - regress2/sygus/cegisunif-depth1-bv.sy - regress2/sygus/ex23.sy - regress2/sygus/icfp_easy_mt_ite.sy - regress2/sygus/inv_gen_n_c11.sy - regress2/sygus/lustre-real.sy - regress2/sygus/max2-univ.sy - regress2/sygus/mpg_guard1-dd.sy - regress2/sygus/nia-max-square.sy - regress2/sygus/no-syntax-test-no-si.sy - regress2/sygus/process-10-vars-2fun.sy - regress2/sygus/process-arg-invariance.sy - regress2/sygus/real-grammar-neg.sy - regress2/sygus/sixfuncs.sy - regress2/sygus/three.sy - regress2/sygus/vcb.sy - regress2/typed_v1l50016-simp.cvc - regress2/uflia-error0.smt2 - regress2/xs-09-16-3-4-1-5.decn.smt - regress2/xs-09-16-3-4-1-5.smt + regress2/DTP_k2_n35_c175_s15.smt2 + regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 + regress2/GEO123+1.minimized.smt2 + regress2/arith/abz5_1400.smt + regress2/arith/lpsat-goal-9.smt2 + regress2/arith/prp-13-24.smt2 + regress2/arith/pursuit-safety-11.smt + regress2/arith/pursuit-safety-12.smt + regress2/arith/qlock-4-10-9.base.cvc.smt2 + regress2/arith/sc-7.base.cvc.smt + regress2/arith/uart-8.base.cvc.smt + regress2/auflia-fuzz06.smt + regress2/bug136.smt + regress2/bug148.smt + regress2/bug394.smt2 + regress2/bug674.smt2 + regress2/bug765.smt2 + regress2/bug812.smt2 + regress2/error0.smt2 + regress2/error1.smt + regress2/friedman_n4_i5.smt + regress2/fuzz_2.smt + regress2/hash_sat_06_19.smt2 + regress2/hash_sat_07_17.smt2 + regress2/hash_sat_09_09.smt2 + regress2/hash_sat_10_09.smt2 + regress2/hole7.cvc + regress2/hole8.cvc + regress2/instance_1444.smt + regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2 + regress2/javafe.ast.WhileStmt.447_no_forall.smt2 + regress2/nl/siegel-nl-bases.smt2 + regress2/ooo.rf6.smt2 + regress2/ooo.tag10.smt2 + regress2/piVC_5581bd.smt2 + regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2 + regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 + regress2/quantifiers/gn-wrong-091018.smt2 + regress2/quantifiers/javafe.ast.ArrayInit.35.smt2 + regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 + regress2/quantifiers/javafe.ast.WhileStmt.447.smt2 + regress2/quantifiers/javafe.tc.CheckCompilationUnit.001.smt2 + regress2/quantifiers/javafe.tc.FlowInsensitiveChecks.682.smt2 + regress2/quantifiers/mutualrec2.cvc + regress2/quantifiers/net-policy-no-time.smt2 + regress2/quantifiers/nunchaku2309663.nun.min.smt2 + regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2 + regress2/strings/cmu-dis-0707-3.smt2 + regress2/strings/cmu-disagree-0707-dd.smt2 + regress2/strings/cmu-prereg-fmf.smt2 + regress2/strings/cmu-repl-len-nterm.smt2 + regress2/strings/norn-dis-0707-3.smt2 + regress2/strings/repl-repl.smt2 + regress2/sygus/MPwL_d1s3.sy + regress2/sygus/array_sum_dd.sy + regress2/sygus/cegisunif-depth1-bv.sy + regress2/sygus/ex23.sy + regress2/sygus/icfp_easy_mt_ite.sy + regress2/sygus/inv_gen_n_c11.sy + regress2/sygus/lustre-real.sy + regress2/sygus/max2-univ.sy + regress2/sygus/mpg_guard1-dd.sy + regress2/sygus/nia-max-square.sy + regress2/sygus/no-syntax-test-no-si.sy + regress2/sygus/process-10-vars-2fun.sy + regress2/sygus/process-arg-invariance.sy + regress2/sygus/real-grammar-neg.sy + regress2/sygus/sixfuncs.sy + regress2/sygus/three.sy + regress2/sygus/vcb.sy + regress2/typed_v1l50016-simp.cvc + regress2/uflia-error0.smt2 + regress2/xs-09-16-3-4-1-5.decn.smt + regress2/xs-09-16-3-4-1-5.smt ) set(regress_3_tests - regress3/bmc-ibm-1.smt - regress3/bmc-ibm-2.smt - regress3/bmc-ibm-5.smt - regress3/bmc-ibm-7.smt - regress3/eq_diamond14.smt - regress3/friedman_n6_i4.smt - regress3/hole9.cvc - regress3/incorrect1.smt - regress3/incorrect2.smt - regress3/pp-regfile.smt - regress3/qwh.35.405.shuffled-as.sat03-1651.smt + regress3/bmc-ibm-1.smt + regress3/bmc-ibm-2.smt + regress3/bmc-ibm-5.smt + regress3/bmc-ibm-7.smt + regress3/eq_diamond14.smt + regress3/friedman_n6_i4.smt + regress3/hole9.cvc + regress3/incorrect1.smt + regress3/incorrect2.smt + regress3/issue2429.smt2 + regress3/pp-regfile.smt + regress3/qwh.35.405.shuffled-as.sat03-1651.smt ) set(regress_4_tests - regress4/C880mul.miter.shuffled-as.sat03-348.smt - regress4/NEQ016_size5.smt - regress4/bug143.smt - regress4/comb2.shuffled-as.sat03-420.smt - regress4/hole10.cvc - regress4/instance_1151.smt + regress4/C880mul.miter.shuffled-as.sat03-348.smt + regress4/NEQ016_size5.smt + regress4/bug143.smt + regress4/comb2.shuffled-as.sat03-420.smt + regress4/hole10.cvc + regress4/instance_1151.smt ) # These tests will not be run. set(regression_disabled_tests - regress0/arith/bug549.cvc - regress0/arith/incorrect1.smt - regress0/arith/integers/arith-int-014.cvc - regress0/arith/integers/arith-int-015.cvc - regress0/arith/integers/arith-int-021.cvc - regress0/arith/integers/arith-int-023.cvc - regress0/arith/integers/arith-int-025.cvc - regress0/arith/integers/arith-int-079.cvc - regress0/arith/integers/arith-interval.cvc - regress0/arith/miplib-opt1217--27.smt - regress0/arith/miplib-pp08a-3000.smt - regress0/arr1.smt - regress0/arr1.smt2 - regress0/arr2.smt + regress0/arith/bug549.cvc + regress0/arith/incorrect1.smt + regress0/arith/integers/arith-int-014.cvc + regress0/arith/integers/arith-int-015.cvc + regress0/arith/integers/arith-int-021.cvc + regress0/arith/integers/arith-int-023.cvc + regress0/arith/integers/arith-int-025.cvc + regress0/arith/integers/arith-int-079.cvc + regress0/arith/integers/arith-interval.cvc + regress0/arith/miplib-opt1217--27.smt + regress0/arith/miplib-pp08a-3000.smt + regress0/arr1.smt + regress0/arr1.smt2 + regress0/arr2.smt # regress0/aufbv/bug348 does not seem to terminate with proofs - regress0/aufbv/bug348.smt - regress0/aufbv/bug349.smt - regress0/aufbv/bug493.smt - regress0/aufbv/dubreva005ue.smt - regress0/aufbv/fifo32bc06k08.smt - regress0/aufbv/fifo32in06k08.delta01.smt - regress0/aufbv/fifo32in06k08.smt - regress0/aufbv/no_init_multi_delete14.smt - regress0/aufbv/try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.smt - regress0/aufbv/wchains010ue.smt - regress0/auflia/fuzz01.smt - regress0/bug2.smt - regress0/bug374.delta01.smt - regress0/bug374.smt - regress0/bv/bug345.smt - regress0/bv/bvcomp.cvc - regress0/bv/bvsmod.smt2 - regress0/bv/core/bitvec0.delta01.smt - regress0/bv/core/bitvec1.smt - regress0/bv/core/bitvec3.smt - regress0/bv/core/bv_eq_diamond11.smt - regress0/bv/core/bv_eq_diamond12.smt - regress0/bv/core/bv_eq_diamond13.smt - regress0/bv/core/bv_eq_diamond14.smt - regress0/bv/core/bv_eq_diamond15.smt - regress0/bv/core/bv_eq_diamond16.smt - regress0/bv/core/bv_eq_diamond17.smt - regress0/bv/core/concat-merge-0.cvc - regress0/bv/core/concat-merge-1.cvc - regress0/bv/core/concat-merge-2.cvc - regress0/bv/core/concat-merge-3.cvc - regress0/bv/core/constant_core.smt2 - regress0/bv/core/equality-00.cvc - regress0/bv/core/equality-01.cvc - regress0/bv/core/equality-02.cvc - regress0/bv/core/equality-03.cvc - regress0/bv/core/equality-03.smt - regress0/bv/core/equality-04.smt - regress0/bv/core/equality-05.smt - regress0/bv/core/ext_con_004_001_1024.smt - regress0/bv/core/extract-concat-0.cvc - regress0/bv/core/extract-concat-1.cvc - regress0/bv/core/extract-concat-10.cvc - regress0/bv/core/extract-concat-11.cvc - regress0/bv/core/extract-concat-2.cvc - regress0/bv/core/extract-concat-3.cvc - regress0/bv/core/extract-concat-4.cvc - regress0/bv/core/extract-concat-5.cvc - regress0/bv/core/extract-concat-6.cvc - regress0/bv/core/extract-concat-7.cvc - regress0/bv/core/extract-concat-8.cvc - regress0/bv/core/extract-concat-9.cvc - regress0/bv/core/extract-constant.cvc - regress0/bv/core/extract-extract-0.cvc - regress0/bv/core/extract-extract-1.cvc - regress0/bv/core/extract-extract-10.cvc - regress0/bv/core/extract-extract-11.cvc - regress0/bv/core/extract-extract-2.cvc - regress0/bv/core/extract-extract-3.cvc - regress0/bv/core/extract-extract-4.cvc - regress0/bv/core/extract-extract-5.cvc - regress0/bv/core/extract-extract-6.cvc - regress0/bv/core/extract-extract-7.cvc - regress0/bv/core/extract-extract-8.cvc - regress0/bv/core/extract-extract-9.cvc - regress0/bv/core/extract-whole-0.cvc - regress0/bv/core/extract-whole-1.cvc - regress0/bv/core/extract-whole-2.cvc - regress0/bv/core/extract-whole-3.cvc - regress0/bv/core/extract-whole-4.cvc - regress0/bv/core/incremental.smt - regress0/bv/core/slice-01.cvc - regress0/bv/core/slice-02.cvc - regress0/bv/core/slice-03.cvc - regress0/bv/core/slice-04.cvc - regress0/bv/core/slice-05.cvc - regress0/bv/core/slice-06.cvc - regress0/bv/core/slice-07.cvc - regress0/bv/core/slice-08.cvc - regress0/bv/core/slice-09.cvc - regress0/bv/core/slice-10.cvc - regress0/bv/core/slice-11.cvc - regress0/bv/core/slice-12.cvc - regress0/bv/core/slice-13.cvc - regress0/bv/core/slice-14.cvc - regress0/bv/core/slice-15.cvc - regress0/bv/core/slice-16.cvc - regress0/bv/core/slice-17.cvc - regress0/bv/core/slice-18.cvc - regress0/bv/core/slice-19.cvc - regress0/bv/core/slice-20.cvc - regress0/bv/fuzz07-delta.smt + regress0/aufbv/bug348.smt + regress0/aufbv/bug349.smt + regress0/aufbv/bug493.smt + regress0/aufbv/dubreva005ue.smt + regress0/aufbv/fifo32bc06k08.smt + regress0/aufbv/fifo32in06k08.delta01.smt + regress0/aufbv/fifo32in06k08.smt + regress0/aufbv/no_init_multi_delete14.smt + regress0/aufbv/try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.smt + regress0/aufbv/wchains010ue.smt + regress0/auflia/fuzz01.smt + regress0/bug2.smt + regress0/bug374.delta01.smt + regress0/bug374.smt + regress0/bv/bug345.smt + regress0/bv/bvcomp.cvc + regress0/bv/bvsmod.smt2 + regress0/bv/core/bitvec0.delta01.smt + regress0/bv/core/bitvec1.smt + regress0/bv/core/bitvec3.smt + regress0/bv/core/bv_eq_diamond11.smt + regress0/bv/core/bv_eq_diamond12.smt + regress0/bv/core/bv_eq_diamond13.smt + regress0/bv/core/bv_eq_diamond14.smt + regress0/bv/core/bv_eq_diamond15.smt + regress0/bv/core/bv_eq_diamond16.smt + regress0/bv/core/bv_eq_diamond17.smt + regress0/bv/core/concat-merge-0.cvc + regress0/bv/core/concat-merge-1.cvc + regress0/bv/core/concat-merge-2.cvc + regress0/bv/core/concat-merge-3.cvc + regress0/bv/core/constant_core.smt2 + regress0/bv/core/equality-00.cvc + regress0/bv/core/equality-01.cvc + regress0/bv/core/equality-02.cvc + regress0/bv/core/equality-03.cvc + regress0/bv/core/equality-03.smt + regress0/bv/core/equality-04.smt + regress0/bv/core/equality-05.smt + regress0/bv/core/ext_con_004_001_1024.smt + regress0/bv/core/extract-concat-0.cvc + regress0/bv/core/extract-concat-1.cvc + regress0/bv/core/extract-concat-10.cvc + regress0/bv/core/extract-concat-11.cvc + regress0/bv/core/extract-concat-2.cvc + regress0/bv/core/extract-concat-3.cvc + regress0/bv/core/extract-concat-4.cvc + regress0/bv/core/extract-concat-5.cvc + regress0/bv/core/extract-concat-6.cvc + regress0/bv/core/extract-concat-7.cvc + regress0/bv/core/extract-concat-8.cvc + regress0/bv/core/extract-concat-9.cvc + regress0/bv/core/extract-constant.cvc + regress0/bv/core/extract-extract-0.cvc + regress0/bv/core/extract-extract-1.cvc + regress0/bv/core/extract-extract-10.cvc + regress0/bv/core/extract-extract-11.cvc + regress0/bv/core/extract-extract-2.cvc + regress0/bv/core/extract-extract-3.cvc + regress0/bv/core/extract-extract-4.cvc + regress0/bv/core/extract-extract-5.cvc + regress0/bv/core/extract-extract-6.cvc + regress0/bv/core/extract-extract-7.cvc + regress0/bv/core/extract-extract-8.cvc + regress0/bv/core/extract-extract-9.cvc + regress0/bv/core/extract-whole-0.cvc + regress0/bv/core/extract-whole-1.cvc + regress0/bv/core/extract-whole-2.cvc + regress0/bv/core/extract-whole-3.cvc + regress0/bv/core/extract-whole-4.cvc + regress0/bv/core/incremental.smt + regress0/bv/core/slice-01.cvc + regress0/bv/core/slice-02.cvc + regress0/bv/core/slice-03.cvc + regress0/bv/core/slice-04.cvc + regress0/bv/core/slice-05.cvc + regress0/bv/core/slice-06.cvc + regress0/bv/core/slice-07.cvc + regress0/bv/core/slice-08.cvc + regress0/bv/core/slice-09.cvc + regress0/bv/core/slice-10.cvc + regress0/bv/core/slice-11.cvc + regress0/bv/core/slice-12.cvc + regress0/bv/core/slice-13.cvc + regress0/bv/core/slice-14.cvc + regress0/bv/core/slice-15.cvc + regress0/bv/core/slice-16.cvc + regress0/bv/core/slice-17.cvc + regress0/bv/core/slice-18.cvc + regress0/bv/core/slice-19.cvc + regress0/bv/core/slice-20.cvc + regress0/bv/fuzz07-delta.smt # Proof checking takes too long. Add this back. FIXME - regress0/bv/fuzz15.delta01.smt + regress0/bv/fuzz15.delta01.smt ### - regress0/bv/fuzz15.smt - regress0/bv/fuzz16.smt - regress0/bv/fuzz17.smt - regress0/bv/incorrect1.delta01.smt - regress0/bv/incorrect1.smt - regress0/bv/inequality00.smt2 - regress0/bv/inequality01.smt2 - regress0/bv/inequality02.smt2 - regress0/bv/inequality03.smt2 - regress0/bv/inequality04.smt2 - regress0/bv/inequality05.smt2 - regress0/bv/test00.smt - regress0/cvc3-bug15.cvc + regress0/bv/fuzz15.smt + regress0/bv/fuzz16.smt + regress0/bv/fuzz17.smt + regress0/bv/incorrect1.delta01.smt + regress0/bv/incorrect1.smt + regress0/bv/inequality00.smt2 + regress0/bv/inequality01.smt2 + regress0/bv/inequality02.smt2 + regress0/bv/inequality03.smt2 + regress0/bv/inequality04.smt2 + regress0/bv/inequality05.smt2 + regress0/bv/test00.smt + regress0/cvc3-bug15.cvc # regress0/datatypes/datatype-dump.cvc (FIXME #1649) regress0/datatypes/datatype-dump.cvc - regress0/decision/uflia-xs-09-16-3-4-1-5.smt - regress0/decision/wchains010ue.smt - regress0/incorrect1.smt - regress0/ite.smt2 - regress0/ite_arith.smt2 - regress0/lemmas/fischer3-mutex-16.smt - regress0/nl/all-logic.smt2 - regress0/quantifiers/qbv-multi-lit-uge.smt2 - regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 - regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 - regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 - regress0/rewriterules/datatypes_clark.smt2 - regress0/rewriterules/length.smt2 - regress0/rewriterules/length_gen_n.smt2 - regress0/rewriterules/length_gen_n_lemma.smt2 - regress0/rewriterules/length_trick2.smt2 - regress0/rewriterules/native_datatypes.smt2 - regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2 - regress0/sets/setel-eq.smt2 - regress0/sets/sets-new.smt2 - regress0/sets/sets-testlemma-ints.smt2 - regress0/sets/sets-testlemma-reals.smt2 - regress0/sygus/sygus-uf.sy - regress0/symmetric.smt - regress0/tptp/BOO003-4.p - regress0/tptp/BOO027-1.p - regress0/tptp/MGT031-1.p - regress0/tptp/NLP114-1.p - regress0/tptp/SYN075+1.p - regress0/uf/PEQ018_size4.smt - regress0/uf/SEQ032_size2.smt - regress0/uf/iso_icl_repgen004.smt - regress0/uflia/diseqprop.01.smt - regress0/uflia/diseqprop.02.smt - regress0/uflia/diseqprop.03.smt - regress0/uflia/diseqprop.04.smt - regress0/uflia/diseqprop.05.smt - regress0/uflia/diseqprop.06.smt - regress0/uflia/xs-09-16-3-4-1-5.delta05.smt - regress0/uflra/pb_real_10_0200_10_25.smt - regress0/uflra/pb_real_10_0200_10_27.smt + regress0/decision/uflia-xs-09-16-3-4-1-5.smt + regress0/decision/wchains010ue.smt + regress0/incorrect1.smt + regress0/ite.smt2 + regress0/ite_arith.smt2 + regress0/lemmas/fischer3-mutex-16.smt + regress0/nl/all-logic.smt2 + regress0/quantifiers/qbv-multi-lit-uge.smt2 + regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 + regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 + regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 + regress0/rewriterules/datatypes_clark.smt2 + regress0/rewriterules/length.smt2 + regress0/rewriterules/length_gen_n.smt2 + regress0/rewriterules/length_gen_n_lemma.smt2 + regress0/rewriterules/length_trick2.smt2 + regress0/rewriterules/native_datatypes.smt2 + regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2 + regress0/sets/setel-eq.smt2 + regress0/sets/sets-new.smt2 + regress0/sets/sets-testlemma-ints.smt2 + regress0/sets/sets-testlemma-reals.smt2 + regress0/sygus/sygus-uf.sy + regress0/symmetric.smt + regress0/tptp/BOO003-4.p + regress0/tptp/BOO027-1.p + regress0/tptp/MGT031-1.p + regress0/tptp/NLP114-1.p + regress0/tptp/SYN075+1.p + regress0/uf/PEQ018_size4.smt + regress0/uf/SEQ032_size2.smt + regress0/uf/iso_icl_repgen004.smt + regress0/uflia/diseqprop.01.smt + regress0/uflia/diseqprop.02.smt + regress0/uflia/diseqprop.03.smt + regress0/uflia/diseqprop.04.smt + regress0/uflia/diseqprop.05.smt + regress0/uflia/diseqprop.06.smt + regress0/uflia/xs-09-16-3-4-1-5.delta05.smt + regress0/uflra/pb_real_10_0200_10_25.smt + regress0/uflra/pb_real_10_0200_10_27.smt # dejan: disabled these because it's mixed arithmetic and it doesn't go # well when changing theoryof: - regress0/unconstrained/arith2.smt2 - regress0/unconstrained/arith7.smt2 + regress0/unconstrained/arith2.smt2 + regress0/unconstrained/arith7.smt2 ### # lianah: disabled these as the unconstrained terms are no longer # recognized after implementing the divide-by-zero semantics for bv division: - regress0/unconstrained/bvconcat.smt2 - regress0/unconstrained/bvdiv.smt + regress0/unconstrained/bvconcat.smt2 + regress0/unconstrained/bvdiv.smt ### - regress1/arith/arith-int-001.cvc - regress1/arith/arith-int-002.cvc - regress1/arith/arith-int-003.cvc - regress1/arith/arith-int-005.cvc - regress1/arith/arith-int-006.cvc - regress1/arith/arith-int-007.cvc - regress1/arith/arith-int-008.cvc - regress1/arith/arith-int-009.cvc - regress1/arith/arith-int-010.cvc - regress1/arith/arith-int-016.cvc - regress1/arith/arith-int-017.cvc - regress1/arith/arith-int-018.cvc - regress1/arith/arith-int-019.cvc - regress1/arith/arith-int-020.cvc - regress1/arith/arith-int-026.cvc - regress1/arith/arith-int-027.cvc - regress1/arith/arith-int-028.cvc - regress1/arith/arith-int-029.cvc - regress1/arith/arith-int-030.cvc - regress1/arith/arith-int-031.cvc - regress1/arith/arith-int-032.cvc - regress1/arith/arith-int-033.cvc - regress1/arith/arith-int-034.cvc - regress1/arith/arith-int-035.cvc - regress1/arith/arith-int-036.cvc - regress1/arith/arith-int-037.cvc - regress1/arith/arith-int-038.cvc - regress1/arith/arith-int-039.cvc - regress1/arith/arith-int-040.cvc - regress1/arith/arith-int-041.cvc - regress1/arith/arith-int-043.cvc - regress1/arith/arith-int-044.cvc - regress1/arith/arith-int-045.cvc - regress1/arith/arith-int-046.cvc - regress1/arith/arith-int-049.cvc - regress1/arith/arith-int-051.cvc - regress1/arith/arith-int-052.cvc - regress1/arith/arith-int-053.cvc - regress1/arith/arith-int-054.cvc - regress1/arith/arith-int-055.cvc - regress1/arith/arith-int-056.cvc - regress1/arith/arith-int-057.cvc - regress1/arith/arith-int-058.cvc - regress1/arith/arith-int-059.cvc - regress1/arith/arith-int-060.cvc - regress1/arith/arith-int-061.cvc - regress1/arith/arith-int-062.cvc - regress1/arith/arith-int-063.cvc - regress1/arith/arith-int-064.cvc - regress1/arith/arith-int-065.cvc - regress1/arith/arith-int-066.cvc - regress1/arith/arith-int-067.cvc - regress1/arith/arith-int-068.cvc - regress1/arith/arith-int-069.cvc - regress1/arith/arith-int-070.cvc - regress1/arith/arith-int-071.cvc - regress1/arith/arith-int-072.cvc - regress1/arith/arith-int-073.cvc - regress1/arith/arith-int-074.cvc - regress1/arith/arith-int-075.cvc - regress1/arith/arith-int-076.cvc - regress1/arith/arith-int-077.cvc - regress1/arith/arith-int-078.cvc - regress1/arith/arith-int-080.cvc - regress1/arith/arith-int-081.cvc - regress1/arith/arith-int-082.cvc - regress1/arith/arith-int-083.cvc - regress1/arith/arith-int-086.cvc - regress1/arith/arith-int-087.cvc - regress1/arith/arith-int-088.cvc - regress1/arith/arith-int-089.cvc - regress1/arith/arith-int-090.cvc - regress1/arith/arith-int-091.cvc - regress1/arith/arith-int-092.cvc - regress1/arith/arith-int-093.cvc - regress1/arith/arith-int-094.cvc - regress1/arith/arith-int-095.cvc - regress1/arith/arith-int-096.cvc - regress1/arith/arith-int-099.cvc - regress1/arith/arith-int-100.cvc - regress1/auflia/bug337.smt2 - regress1/bug472.smt2 - regress1/bug585.cvc - regress1/bug590.smt2 - regress1/bv/bench_38.delta.smt2 - regress1/crash_burn_locusts.smt2 + regress1/arith/arith-int-001.cvc + regress1/arith/arith-int-002.cvc + regress1/arith/arith-int-003.cvc + regress1/arith/arith-int-005.cvc + regress1/arith/arith-int-006.cvc + regress1/arith/arith-int-007.cvc + regress1/arith/arith-int-008.cvc + regress1/arith/arith-int-009.cvc + regress1/arith/arith-int-010.cvc + regress1/arith/arith-int-016.cvc + regress1/arith/arith-int-017.cvc + regress1/arith/arith-int-018.cvc + regress1/arith/arith-int-019.cvc + regress1/arith/arith-int-020.cvc + regress1/arith/arith-int-026.cvc + regress1/arith/arith-int-027.cvc + regress1/arith/arith-int-028.cvc + regress1/arith/arith-int-029.cvc + regress1/arith/arith-int-030.cvc + regress1/arith/arith-int-031.cvc + regress1/arith/arith-int-032.cvc + regress1/arith/arith-int-033.cvc + regress1/arith/arith-int-034.cvc + regress1/arith/arith-int-035.cvc + regress1/arith/arith-int-036.cvc + regress1/arith/arith-int-037.cvc + regress1/arith/arith-int-038.cvc + regress1/arith/arith-int-039.cvc + regress1/arith/arith-int-040.cvc + regress1/arith/arith-int-041.cvc + regress1/arith/arith-int-043.cvc + regress1/arith/arith-int-044.cvc + regress1/arith/arith-int-045.cvc + regress1/arith/arith-int-046.cvc + regress1/arith/arith-int-049.cvc + regress1/arith/arith-int-051.cvc + regress1/arith/arith-int-052.cvc + regress1/arith/arith-int-053.cvc + regress1/arith/arith-int-054.cvc + regress1/arith/arith-int-055.cvc + regress1/arith/arith-int-056.cvc + regress1/arith/arith-int-057.cvc + regress1/arith/arith-int-058.cvc + regress1/arith/arith-int-059.cvc + regress1/arith/arith-int-060.cvc + regress1/arith/arith-int-061.cvc + regress1/arith/arith-int-062.cvc + regress1/arith/arith-int-063.cvc + regress1/arith/arith-int-064.cvc + regress1/arith/arith-int-065.cvc + regress1/arith/arith-int-066.cvc + regress1/arith/arith-int-067.cvc + regress1/arith/arith-int-068.cvc + regress1/arith/arith-int-069.cvc + regress1/arith/arith-int-070.cvc + regress1/arith/arith-int-071.cvc + regress1/arith/arith-int-072.cvc + regress1/arith/arith-int-073.cvc + regress1/arith/arith-int-074.cvc + regress1/arith/arith-int-075.cvc + regress1/arith/arith-int-076.cvc + regress1/arith/arith-int-077.cvc + regress1/arith/arith-int-078.cvc + regress1/arith/arith-int-080.cvc + regress1/arith/arith-int-081.cvc + regress1/arith/arith-int-082.cvc + regress1/arith/arith-int-083.cvc + regress1/arith/arith-int-086.cvc + regress1/arith/arith-int-087.cvc + regress1/arith/arith-int-088.cvc + regress1/arith/arith-int-089.cvc + regress1/arith/arith-int-090.cvc + regress1/arith/arith-int-091.cvc + regress1/arith/arith-int-092.cvc + regress1/arith/arith-int-093.cvc + regress1/arith/arith-int-094.cvc + regress1/arith/arith-int-095.cvc + regress1/arith/arith-int-096.cvc + regress1/arith/arith-int-099.cvc + regress1/arith/arith-int-100.cvc + regress1/auflia/bug337.smt2 + regress1/bug472.smt2 + regress1/bug585.cvc + regress1/bug590.smt2 + regress1/bv/bench_38.delta.smt2 + regress1/crash_burn_locusts.smt2 # regress1/ho/hoa0102.smt2 results in an assertion failure (see issue #1650). - regress1/ho/hoa0102.smt2 + regress1/ho/hoa0102.smt2 # issue1048-arrays-int-real.smt2 -- different errors on debug and production. - regress1/issue1048-arrays-int-real.smt2 + regress1/issue1048-arrays-int-real.smt2 # ajreynol: disabled these since they give different error messages on # production and debug: - regress1/quantifiers/macro-subtype-param.smt2 - regress1/quantifiers/subtype-param-unk.smt2 - regress1/quantifiers/subtype-param.smt2 + regress1/quantifiers/macro-subtype-param.smt2 + regress1/quantifiers/subtype-param-unk.smt2 + regress1/quantifiers/subtype-param.smt2 ### # regress1/quantifiers/set3.smt2 does not terminate/takes a long time when # doing a coverage build with LFSC. - regress1/quantifiers/set3.smt2 - regress1/rels/garbage_collect.cvc - regress1/rewriterules/datatypes2.smt2 - regress1/rewriterules/datatypes3.smt2 - regress1/rewriterules/datatypes_clark_quantification.smt2 - regress1/rewriterules/length_gen_010.smt2 - regress1/rewriterules/length_gen_010_lemma.smt2 - regress1/rewriterules/length_gen_080.smt2 - regress1/rewriterules/length_gen_160_lemma.smt2 - regress1/rewriterules/length_gen_inv_160.smt2 - regress1/rewriterules/length_trick3.smt2 - regress1/rewriterules/length_trick3_int.smt2 - regress1/rewriterules/set_A_new_fast_tableau-base.smt2 - regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2 - regress1/rewriterules/test_guards.smt2 - regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2 - regress1/sets/setofsets-disequal.smt2 - regress1/simple-rdl-definefun.smt2 - regress1/sygus/Base16_1.sy - regress1/sygus/enum-test.sy - regress1/sygus/inv_gen_fig8.sy - regress2/arith/arith-int-098.cvc - regress2/arith/miplib-opt1217--27.smt2 - regress2/arith/miplib-pp08a-3000.smt2 - regress2/bug396.smt2 - regress2/nl/dumortier-050317.smt2 - regress2/nl/nt-lemmas-bad.smt2 - regress2/quantifiers/ForElimination-scala-9.smt2 - regress2/quantifiers/small-bug1-fixpoint-3.smt2 - regress2/xs-11-20-5-2-5-3.smt - regress2/xs-11-20-5-2-5-3.smt2 + regress1/quantifiers/set3.smt2 + regress1/rels/garbage_collect.cvc + regress1/rewriterules/datatypes2.smt2 + regress1/rewriterules/datatypes3.smt2 + regress1/rewriterules/datatypes_clark_quantification.smt2 + regress1/rewriterules/length_gen_010.smt2 + regress1/rewriterules/length_gen_010_lemma.smt2 + regress1/rewriterules/length_gen_080.smt2 + regress1/rewriterules/length_gen_160_lemma.smt2 + regress1/rewriterules/length_gen_inv_160.smt2 + regress1/rewriterules/length_trick3.smt2 + regress1/rewriterules/length_trick3_int.smt2 + regress1/rewriterules/set_A_new_fast_tableau-base.smt2 + regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2 + regress1/rewriterules/test_guards.smt2 + regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2 + regress1/sets/setofsets-disequal.smt2 + regress1/simple-rdl-definefun.smt2 + regress1/sygus/Base16_1.sy + regress1/sygus/enum-test.sy + regress1/sygus/inv_gen_fig8.sy + regress2/arith/arith-int-098.cvc + regress2/arith/miplib-opt1217--27.smt2 + regress2/arith/miplib-pp08a-3000.smt2 + regress2/bug396.smt2 + regress2/nl/dumortier-050317.smt2 + regress2/nl/nt-lemmas-bad.smt2 + regress2/quantifiers/ForElimination-scala-9.smt2 + regress2/quantifiers/small-bug1-fixpoint-3.smt2 + regress2/xs-11-20-5-2-5-3.smt + regress2/xs-11-20-5-2-5-3.smt2 ) get_target_property(path_to_cvc4 cvc4-bin RUNTIME_OUTPUT_DIRECTORY) diff --git a/test/system/CMakeLists.txt b/test/system/CMakeLists.txt index 0ae2806d4..291916082 100644 --- a/test/system/CMakeLists.txt +++ b/test/system/CMakeLists.txt @@ -11,7 +11,7 @@ set(CVC4_SYSTEM_TEST_FLAGS macro(cvc4_add_system_test name) # add_executable(${name} ${ARGN}) add_executable(${name} ${name}.cpp) - target_link_libraries(${name} main cvc4compat) + target_link_libraries(${name} main) target_compile_definitions(${name} PRIVATE ${CVC4_SYSTEM_TEST_FLAGS}) add_test(system/${name} ${CMAKE_CURRENT_BINARY_DIR}/${name}) set_tests_properties(system/${name} PROPERTIES LABELS "system") @@ -28,4 +28,4 @@ cvc4_add_system_test(sep_log_api) cvc4_add_system_test(smt2_compliance) cvc4_add_system_test(statistics) cvc4_add_system_test(two_smt_engines) -#TODO java test (needs bindings) +# TODO: Move CVC4JavaTest.java to test/java and delete run_java_test (after full cmake migration) |