regress0/arith/arith-strict.smt2
regress0/arith/arith-tighten-1.smt2
regress0/arith/arith-tighten-2.smt2
- regress0/arith/arith.01.cvc
- regress0/arith/arith.02.cvc
- regress0/arith/arith.03.cvc
+ regress0/arith/arith.01.cvc.smt2
+ regress0/arith/arith.02.cvc.smt2
+ regress0/arith/arith.03.cvc.smt2
regress0/arith/bug443.delta01.smtv1.smt2
regress0/arith/bug547.2.smt2
- regress0/arith/bug549.cvc
+ regress0/arith/bug549.cvc.smt2
regress0/arith/bug569.smt2
regress0/arith/delta-minimized-row-vector-bug.smtv1.smt2
regress0/arith/div-chainable.smt2
regress0/arith/integers/ackermann4.smt2
regress0/arith/integers/ackermann5.smt2
regress0/arith/integers/ackermann6.smt2
- 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-042.cvc
- regress0/arith/integers/arith-int-042.min.cvc
- regress0/arith/integers/arith-int-079.cvc
- regress0/arith/integers/arith-interval.cvc
+ regress0/arith/integers/arith-int-014.cvc.smt2
+ regress0/arith/integers/arith-int-015.cvc.smt2
+ regress0/arith/integers/arith-int-021.cvc.smt2
+ regress0/arith/integers/arith-int-023.cvc.smt2
+ regress0/arith/integers/arith-int-025.cvc.smt2
+ regress0/arith/integers/arith-int-042.cvc.smt2
+ regress0/arith/integers/arith-int-042.min.cvc.smt2
+ regress0/arith/integers/arith-int-079.cvc.smt2
+ regress0/arith/integers/arith-interval.cvc.smt2
regress0/arith/integers/issue6146-stale-vars.smt2
regress0/arith/issue1399.smt2
regress0/arith/issue3412.smt2
regress0/arith/issue5761-ppr.smt2
regress0/arith/ite-lift.smt2
regress0/arith/leq.01.smtv1.smt2
- regress0/arith/miplib.cvc
- regress0/arith/miplib2.cvc
- regress0/arith/miplib4.cvc
+ regress0/arith/miplib.cvc.smt2
+ regress0/arith/miplib2.cvc.smt2
+ regress0/arith/miplib4.cvc.smt2
regress0/arith/miplibtrick.smtv1.smt2
regress0/arith/mod-simp.smt2
regress0/arith/mod.01.smt2
regress0/arrays/bug3020.smt2
regress0/arrays/bug4957.smt2
regress0/arrays/bug637.delta.smt2
- regress0/arrays/constarr.cvc
+ regress0/arrays/constarr.cvc.smt2
regress0/arrays/constarr.smt2
- regress0/arrays/constarr2.cvc
+ regress0/arrays/constarr2.cvc.smt2
regress0/arrays/constarr2.smt2
regress0/arrays/incorrect1.smtv1.smt2
regress0/arrays/incorrect10.smtv1.smt2
regress0/arrays/issue3813-massign-assert.smt2
regress0/arrays/issue3814.smt2
regress0/arrays/issue4927-unsat-cores.smt2
+ regress0/arrays/issue7596-define-array-uminus.smt2
regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2
regress0/arrays/x2.smtv1.smt2
regress0/arrays/x3.smtv1.smt2
regress0/aufbv/bug493.smtv1.smt2
regress0/aufbv/bug509.smtv1.smt2
regress0/aufbv/bug580.delta.smt2
+ regress0/aufbv/cee-small-shared-eq.smt2
regress0/aufbv/diseqprop.01.smtv1.smt2
regress0/aufbv/dubreva005ue.delta01.smtv1.smt2
regress0/aufbv/fifo32bc06k08.delta01.smtv1.smt2
regress0/auflia/fuzz05.smtv1.smt2
regress0/auflia/x2.smtv1.smt2
regress0/bool/issue1978.smt2
- regress0/boolean-prec.cvc
+ regress0/bool/issue6717-ite-rewrite.smt2
+ regress0/boolean-prec.cvc.smt2
regress0/boolean-terms-bug-array.smt2
regress0/boolean-terms-kernel1.smt2
- regress0/boolean-terms.cvc
+ regress0/boolean-terms.cvc.smt2
regress0/bt-test-00.smt2
regress0/bt-test-01.smt2
regress0/bug1247.smt2
regress0/bug217.smt2
regress0/bug220.smt2
regress0/bug239.smtv1.smt2
- regress0/bug274.cvc
+ regress0/bug274.cvc.smt2
regress0/bug288.smtv1.smt2
regress0/bug288b.smtv1.smt2
regress0/bug288c.smtv1.smt2
regress0/bug303.smt2
- regress0/bug310.cvc
- regress0/bug32.cvc
- regress0/bug322.cvc
- regress0/bug322b.cvc
+ regress0/bug310.cvc.smt2
+ regress0/bug32.cvc.smt2
+ regress0/bug322.cvc.smt2
+ regress0/bug322b.cvc.smt2
regress0/bug339.smt2
regress0/bug365.smt2
regress0/bug382.smt2
regress0/bug421b.smt2
regress0/bug480.smt2
regress0/bug484.smt2
- regress0/bug486.cvc
+ regress0/bug486.cvc.smt2
regress0/bug49.smtv1.smt2
regress0/bug512.minimized.smt2
regress0/bug521.minimized.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/bug586.cvc.smt2
+ regress0/bug595.cvc.smt2
+ regress0/bug596.cvc.smt2
+ regress0/bug596b.cvc.smt2
+ regress0/bug605.cvc.smt2
regress0/bug639.smt2
regress0/buggy-ite.smt2
regress0/bv/ackermann1.smt2
regress0/bv/bug440.smtv1.smt2
regress0/bv/bug733.smt2
regress0/bv/bug734.smt2
+ regress0/bv/bv-abstr-bug2.smt2
+ regress0/bv/bv-int-collapse1.smt2
+ regress0/bv/bv-int-collapse2.smt2
+ regress0/bv/bv-options4.smt2
+ regress0/bv/bv-to-bool1.smtv1.smt2
+ regress0/bv/bv-to-bool2.smt2
+ regress0/bv/bv2nat-ground-c.smt2
+ regress0/bv/bv2nat-simp-range.smt2
+ regress0/bv/bv_to_int1.smt2
regress0/bv/bv_to_int_5230_binary.smt2
regress0/bv/bv_to_int_5230_missing_op.smt2
regress0/bv/bv_to_int_5230_shift_const.smt2
regress0/bv/bv_to_int_5293_1.smt2
regress0/bv/bv_to_int_5293_2.smt2
regress0/bv/bv_to_int_bvmul2.smt2
- regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
regress0/bv/bv_to_int_bvuf_to_intuf.smt2
+ regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
regress0/bv/bv_to_int_elim_err.smt2
regress0/bv/bv_to_int_zext.smt2
- regress0/bv/bv_to_int1.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-options4.smt2
- regress0/bv/bv-to-bool1.smtv1.smt2
- regress0/bv/bv-to-bool2.smt2
- regress0/bv/bv2nat-ground-c.smt2
- regress0/bv/bv2nat-simp-range.smt2
- regress0/bv/bvcomp.cvc
+ regress0/bv/bvcomp.cvc.smt2
regress0/bv/bvmul-pow2-only.smt2
- regress0/bv/bvsimple.cvc
+ regress0/bv/bvproof1.smt2
+ regress0/bv/bvproof2.smt2
+ regress0/bv/bvproof3.smt2
+ regress0/bv/bvsimple.cvc.smt2
regress0/bv/bvsmod.smt2
regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smtv1.smt2
regress0/bv/core/a78test0002.smtv1.smt2
regress0/bv/core/slice-18.smtv1.smt2
regress0/bv/core/slice-19.smtv1.smt2
regress0/bv/core/slice-20.smtv1.smt2
- regress0/bv/div_mod.cvc
+ regress0/bv/div_mod.cvc.smt2
regress0/bv/divtest_2_5.smt2
regress0/bv/divtest_2_6.smt2
regress0/bv/eager-force-logic.smt2
regress0/bv/inequality04.smt2
regress0/bv/inequality05.smt2
regress0/bv/int_to_bv_err_on_demand_1.smt2
+ regress0/bv/int_to_bv_model.smt2
+ regress0/bv/int_to_bv_model2.smt2
regress0/bv/issue-4075.smt2
regress0/bv/issue-4076.smt2
regress0/bv/issue-4130.smt2
regress0/bv/issue3621.smt2
+ regress0/bv/issue5396.smt2
regress0/bv/mul-neg-unsat.smt2
regress0/bv/mul-negpow2.smt2
regress0/bv/mult-pow2-negative.smt2
regress0/bv/pr4993-bvugt-bvurem-a.smt2
regress0/bv/pr4993-bvugt-bvurem-b.smt2
- regress0/bv/sizecheck.cvc
+ regress0/bv/reset-assertions-assert-input.smt2
+ regress0/bv/sizecheck.cvc.smt2
regress0/bv/smtcompbug.smtv1.smt2
regress0/bv/test-bv_intro_pow2.smt2
regress0/bv/unsound1-reduced.smt2
regress0/chained-equality.smt2
regress0/constant-rewrite.smtv1.smt2
- regress0/cvc-rerror-print.cvc
- regress0/cvc3-bug15.cvc
- 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/cores/issue3455.smt2
+ regress0/cores/issue3651.smt2
+ regress0/cores/issue4925.smt2
+ regress0/cores/issue4971-0.smt2
+ regress0/cores/issue4971-1.smt2
+ regress0/cores/issue4971-2.smt2
+ regress0/cores/issue4971-3.smt2
+ regress0/cores/issue5079.smt2
+ regress0/cores/issue5234-uc-ua.smt2
+ regress0/cores/issue5238.smt2
+ regress0/cores/issue5902.smt2
+ regress0/cores/issue5908.smt2
+ regress0/cvc-rerror-print.cvc.smt2
+ regress0/cvc3-bug15.cvc.smt2
+ regress0/cvc3.userdoc.01.cvc.smt2
+ regress0/cvc3.userdoc.02.cvc.smt2
+ regress0/cvc3.userdoc.03.cvc.smt2
+ regress0/cvc3.userdoc.04.cvc.smt2
+ regress0/cvc3.userdoc.05.cvc.smt2
+ regress0/cvc3.userdoc.06.cvc.smt2
regress0/datatypes/4482-unc-simp-one.smt2
- regress0/datatypes/boolean-equality.cvc
- regress0/datatypes/boolean-terms-datatype.cvc
- regress0/datatypes/boolean-terms-parametric-datatype-1.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/boolean-equality.cvc.smt2
+ regress0/datatypes/boolean-terms-datatype.cvc.smt2
+ regress0/datatypes/boolean-terms-parametric-datatype-1.cvc.smt2
+ regress0/datatypes/boolean-terms-record.cvc.smt2
+ regress0/datatypes/boolean-terms-rewrite.cvc.smt2
+ regress0/datatypes/boolean-terms-tuple.cvc.smt2
+ regress0/datatypes/bug286.cvc.smt2
+ regress0/datatypes/bug438.cvc.smt2
+ regress0/datatypes/bug438b.cvc.smt2
regress0/datatypes/bug597-rbt.smt2
regress0/datatypes/bug604.smt2
regress0/datatypes/bug625.smt2
+ regress0/datatypes/canExp-dtPendingMerge.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/data-nested-codata.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/datatype-dump.cvc.smt2
+ regress0/datatypes/datatype.cvc.smt2
+ regress0/datatypes/datatype0.cvc.smt2
+ regress0/datatypes/datatype1.cvc.smt2
+ regress0/datatypes/datatype13.cvc.smt2
+ regress0/datatypes/datatype2.cvc.smt2
+ regress0/datatypes/datatype3.cvc.smt2
+ regress0/datatypes/datatype4.cvc.smt2
regress0/datatypes/dt-2.6.smt2
regress0/datatypes/dt-different-params.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/empty_tuprec.cvc.smt2
regress0/datatypes/example-dailler-min.smt2
regress0/datatypes/is_test.smt2
regress0/datatypes/issue1433.smt2
- regress0/datatypes/issue2838.cvc
+ regress0/datatypes/issue2838.cvc.smt2
+ regress0/datatypes/issue4393-cdt-model.smt2
regress0/datatypes/issue5280-no-nrec.smt2
regress0/datatypes/jsat-2.6.smt2
regress0/datatypes/list-bool.smt2
+ regress0/datatypes/list-update.smt2
+ regress0/datatypes/list-update-sat.smt2
regress0/datatypes/model-subterms-min.smt2
- regress0/datatypes/mutually-recursive.cvc
- regress0/datatypes/pair-bool-bool.cvc
+ regress0/datatypes/mutually-recursive.cvc.smt2
+ regress0/datatypes/pair-bool-bool.cvc.smt2
regress0/datatypes/pair-real-bool.smt2
- regress0/datatypes/parametric-alt-list.cvc
- regress0/datatypes/rec1.cvc
- regress0/datatypes/rec2.cvc
- regress0/datatypes/rec4.cvc
- regress0/datatypes/rewriter.cvc
+ regress0/datatypes/parametric-alt-list.cvc.smt2
+ regress0/datatypes/rec1.cvc.smt2
+ regress0/datatypes/rec2.cvc.smt2
+ regress0/datatypes/rec4.cvc.smt2
+ regress0/datatypes/rewriter.cvc.smt2
regress0/datatypes/sc-cdt1.smt2
- regress0/datatypes/some-boolean-tests.cvc
+ regress0/datatypes/some-boolean-tests.cvc.smt2
regress0/datatypes/stream-singleton.smt2
regress0/datatypes/tenum-bug.smt2
- regress0/datatypes/Test1-tup-mp.cvc
- regress0/datatypes/tree-get-value.cvc
- regress0/datatypes/tuple-model.cvc
- regress0/datatypes/tuple-no-clash.cvc
- regress0/datatypes/tuple-record-bug.cvc
- regress0/datatypes/tuple.cvc
+ regress0/datatypes/Test1-tup-mp.cvc.smt2
+ regress0/datatypes/tree-get-value.cvc.smt2
+ regress0/datatypes/tuple-model.cvc.smt2
+ regress0/datatypes/tuple-no-clash.cvc.smt2
+ regress0/datatypes/tuple-record-bug.cvc.smt2
+ regress0/datatypes/tuple.cvc.smt2
+ regress0/datatypes/tuple_update.smt2
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/datatypes/typed_v10l30054.cvc.smt2
+ regress0/datatypes/typed_v1l80005.cvc.smt2
+ regress0/datatypes/typed_v2l30079.cvc.smt2
+ regress0/datatypes/typed_v3l20092.cvc.smt2
+ regress0/datatypes/typed_v5l30069.cvc.smt2
+ regress0/datatypes/v10l40099.cvc.smt2
+ regress0/datatypes/v2l40025.cvc.smt2
+ regress0/datatypes/v3l60006.cvc.smt2
+ regress0/datatypes/v5l30058.cvc.smt2
+ regress0/datatypes/wrong-sel-simp.cvc.smt2
regress0/decision/aufbv-fuzz01.smtv1.smt2
regress0/decision/bitvec0.delta01.smtv1.smt2
regress0/decision/bitvec0.smtv1.smt2
regress0/define-fun-model.smt2
regress0/distinct.smtv1.smt2
regress0/dump-unsat-core-full.smt2
+ regress0/echo.smt2
+ regress0/eqrange0.smt2
regress0/eqrange1.smt2
regress0/eqrange2.smt2
regress0/eqrange3.smt2
regress0/expect/scrub.01.smtv1.smt2
regress0/expect/scrub.03.smt2
- regress0/expect/scrub.06.cvc
+ regress0/expect/scrub.06.cvc.smt2
regress0/expect/scrub.08.sy
regress0/expect/scrub.09.p
regress0/flet.smtv1.smt2
regress0/fmf/array_card.smt2
regress0/fmf/Arrow_Order-smtlib.778341.smtv1.smt2
regress0/fmf/bounded_sets.smt2
- regress0/fmf/bug-041417-set-options.cvc
+ regress0/fmf/bug-041417-set-options.cvc.smt2
regress0/fmf/bug782.smt2
regress0/fmf/cruanes-no-minimal-unk.smt2
regress0/fmf/fc-simple.smt2
regress0/fmf/krs-sat.smt2
regress0/fmf/no-minimal-sat.smt2
regress0/fmf/QEpres-uf.855035.smtv1.smt2
- regress0/fmf/quant_real_univ.cvc
+ regress0/fmf/quant_real_univ.cvc.smt2
regress0/fmf/sat-logic.smt2
regress0/fmf/sc_bad_model_1221.smt2
regress0/fmf/sort-infer-typed-082718.smt2
regress0/fmf/tail_rec.smt2
regress0/fp/abs-unsound.smt2
regress0/fp/abs-unsound2.smt2
+ regress0/fp/bvcomp-rewrite.smt2
regress0/fp/down-cast-RNA.smt2
regress0/fp/ext-rew-test.smt2
regress0/fp/from_ubv.smt2
regress0/fp/issue3619.smt2
regress0/fp/issue4277-assign-func.smt2
regress0/fp/issue5511.smt2
+ regress0/fp/issue5734.smt2
regress0/fp/issue6164.smt2
+ regress0/fp/issue7002.smt2
+ regress0/fp/issue7569.smt2
+ regress0/fp/proj-issue329-prereg-context.smt2
regress0/fp/rti_3_5_bug.smt2
regress0/fp/simple.smt2
+ regress0/fp/word-blast.smt2
regress0/fp/wrong-model.smt2
regress0/fuzz_1.smtv1.smt2
regress0/fuzz_3.smtv1.smt2
regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p
regress0/ho/cong-full-apply.smt2
regress0/ho/cong.smt2
+ regress0/ho/datatype-field-ho.smt2
regress0/ho/declare-fun-variants.smt2
regress0/ho/def-fun-flatten.smt2
regress0/ho/ext-finite-unsat.smt2
regress0/ho/issue4477.smt2
regress0/ho/issue4990-care-graph.smt2
regress0/ho/issue5233-part1-usort-owner.smt2
+ regress0/ho/issue5371.smt2
+ regress0/ho/issue5741-1-cg-model.smt2
+ regress0/ho/issue5741-3-cg-model.smt2
+ regress0/ho/issue5744-cg-model.smt2
+ regress0/ho/issue6526.smt2
+ regress0/ho/issue6536.smt2
regress0/ho/ite-apply-eq.smt2
regress0/ho/lambda-equality-non-canon.smt2
+ regress0/ho/lazy-lambda-model.smt2
regress0/ho/match-middle.smt2
regress0/ho/modulo-func-equality.smt2
+ regress0/ho/qgu-fuzz-ho-1-dd.smt2
+ regress0/ho/qgu-fuzz-ho-2-dd-no-ext.smt2
regress0/ho/shadowing-defs.smt2
+ regress0/ho/simple-conf-lazy-lambda-lift.smt2
+ regress0/ho/simple-conf-lazy-lambda-lift-app.smt2
regress0/ho/simple-matching-partial.smt2
regress0/ho/simple-matching.smt2
regress0/ho/trans.smt2
regress0/incorrect1.smtv1.smt2
regress0/ineq_basic.smtv1.smt2
regress0/ineq_slack.smtv1.smt2
+ regress0/int-to-bv/basic.smt2
+ regress0/int-to-bv/neg-consts.smt2
+ regress0/int-to-bv/not-enough-bits.smt2
+ regress0/int-to-bv/overflow.smt2
regress0/issue1063-overloading-dt-cons.smt2
regress0/issue1063-overloading-dt-fun.smt2
regress0/issue1063-overloading-dt-sel.smt2
regress0/issue5540-2-dump-model.smt2
regress0/issue5540-model-decls.smt2
regress0/issue5550-num-children.smt2
+ regress0/issue5736.smt2
+ regress0/issue5743.smt2
+ regress0/issue5947.smt2
+ regress0/issue6605-2-abd-triv.smt2
+ regress0/issue6738.smt2
+ regress0/issue6741.smt2
regress0/ite_arith.smt2
regress0/ite_real_int_type.smtv1.smt2
regress0/ite_real_valid.smtv1.smt2
- regress0/ite.cvc
+ regress0/ite.cvc.smt2
regress0/ite.smt2
regress0/ite2.smt2
regress0/ite3.smt2
regress0/lemmas/fs_not_sc_seen.induction.smtv1.smt2
regress0/lemmas/mode_cntrl.induction.smtv1.smt2
regress0/lemmas/sc_init_frame_gap.induction.smtv1.smt2
- regress0/let.cvc
+ regress0/let.cvc.smt2
regress0/let.smtv1.smt2
regress0/let2.smtv1.smt2
- regress0/logops.01.cvc
- regress0/logops.02.cvc
- regress0/logops.03.cvc
- regress0/logops.04.cvc
- regress0/logops.05.cvc
+ regress0/logops.01.cvc.smt2
+ regress0/logops.02.cvc.smt2
+ regress0/logops.03.cvc.smt2
+ regress0/logops.04.cvc.smt2
+ regress0/logops.05.cvc.smt2
regress0/model-core.smt2
regress0/models-print-1.smt2
regress0/models-print-2.smt2
regress0/nl/nta/sin-sym.smt2
regress0/nl/nta/sqrt-simple.smt2
regress0/nl/nta/tan-rewrite.smt2
+ regress0/nl/pow2-native-0.smt2
+ regress0/nl/pow2-native-1.smt2
+ regress0/nl/pow2-native-2.smt2
+ regress0/nl/pow2-native-3.smt2
+ regress0/nl/pow2-pow.smt2
+ regress0/nl/pow2-pow-isabelle.smt2
regress0/nl/real-as-int.smt2
regress0/nl/real-div-ufnra.smt2
regress0/nl/sin-cos-346-b-chunk-0169.smt2
regress0/nl/very-simple-unsat.smt2
regress0/opt-abd-no-use.smt2
regress0/options/ast-and-sexpr.smt2
- regress0/options/invalid_dump.smt2
+ regress0/options/didyoumean.smt2
+ regress0/options/help.smt2
+ regress0/options/interactive-mode.smt2
+ regress0/options/set-after-init.smt2
regress0/options/set-and-get-options.smt2
+ regress0/options/statistics.smt2
+ regress0/options/stream-printing.smt2
+ regress0/options/version.smt2
regress0/parallel-let.smt2
regress0/parser/as.smt2
regress0/parser/bv_arity_smt2.6.smt2
regress0/parser/force_logic_set_logic.smt2
regress0/parser/force_logic_success.smt2
regress0/parser/issue5163.smt2
+ regress0/parser/issue6908-get-value-uc.smt2
+ regress0/parser/issue7274.smt2
regress0/parser/linear_arithmetic_err1.smt2
regress0/parser/linear_arithmetic_err2.smt2
regress0/parser/linear_arithmetic_err3.smt2
+ regress0/parser/named-attr-error.smt2
+ regress0/parser/named-attr.smt2
+ regress0/parser/proj-issue370-push-pop-global.smt2
+ regress0/parser/quoted-define-fun.smt2
regress0/parser/shadow_fun_symbol_all.smt2
regress0/parser/shadow_fun_symbol_nirat.smt2
regress0/parser/strings20.smt2
regress0/parser/strings25.smt2
regress0/parser/to_fp.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/precedence/and-not.cvc.smt2
+ regress0/precedence/and-xor.cvc.smt2
+ regress0/precedence/bool-cmp.cvc.smt2
+ regress0/precedence/cmp-plus.cvc.smt2
+ regress0/precedence/eq-fun.cvc.smt2
+ regress0/precedence/iff-assoc.cvc.smt2
+ regress0/precedence/iff-implies.cvc.smt2
+ regress0/precedence/implies-assoc.cvc.smt2
+ regress0/precedence/implies-iff.cvc.smt2
+ regress0/precedence/implies-or.cvc.smt2
+ regress0/precedence/not-and.cvc.smt2
+ regress0/precedence/not-eq.cvc.smt2
+ regress0/precedence/or-implies.cvc.smt2
+ regress0/precedence/or-xor.cvc.smt2
+ regress0/precedence/plus-mult.cvc.smt2
+ regress0/precedence/xor-and.cvc.smt2
+ regress0/precedence/xor-assoc.cvc.smt2
+ regress0/precedence/xor-or.cvc.smt2
regress0/preprocess/circuit-prop.smt2
regress0/preprocess/issue5729-rewritten-assertions.smt2
regress0/preprocess/issue5943-non-clausal-simp.smt2
- 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/preprocess/issue6754-tpp.smt2
+ regress0/preprocess/preprocess_00.cvc.smt2
+ regress0/preprocess/preprocess_01.cvc.smt2
+ regress0/preprocess/preprocess_02.cvc.smt2
+ regress0/preprocess/preprocess_03.cvc.smt2
+ regress0/preprocess/preprocess_04.cvc.smt2
+ regress0/preprocess/preprocess_05.cvc.smt2
+ regress0/preprocess/preprocess_06.cvc.smt2
+ regress0/preprocess/preprocess_07.cvc.smt2
+ regress0/preprocess/preprocess_08.cvc.smt2
+ regress0/preprocess/preprocess_09.cvc.smt2
+ regress0/preprocess/preprocess_10.cvc.smt2
+ regress0/preprocess/preprocess_11.cvc.smt2
+ regress0/preprocess/preprocess_12.cvc.smt2
+ regress0/preprocess/preprocess_13.cvc.smt2
+ regress0/preprocess/preprocess_14.cvc.smt2
+ regress0/preprocess/preprocess_15.cvc.smt2
+ regress0/preprocess/proj-issue304-circuit-prop-xor.smt2
+ regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2
+ regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2
+ regress0/preprocess/proj-issue305-circuit-prop-ite-c.smt2
+ regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2
+ regress0/preprocess/proj-issue309-circuit-prop-ite.smt2
+ regress0/preprocess/proj-issue332-circuit-prop-xor.smt2
regress0/print_define_fun_internal.smt2
- regress0/print_lambda.cvc
- regress0/print_model.cvc
+ regress0/print_lambda.cvc.smt2
+ regress0/print_model.cvc.smt2
regress0/printer/bv_consts_bin.smt2
regress0/printer/bv_consts_dec.smt2
regress0/printer/empty_sort.smt2
regress0/printer/empty_symbol_name.smt2
regress0/printer/let_shadowing.smt2
regress0/printer/symbol_starting_w_digit.smt2
- regress0/printer/tuples_and_records.cvc
+ regress0/printer/tuples_and_records.cvc.smt2
+ regress0/proj-issue307-get-value-re.smt2
+ regress0/proofs/cyclic-ucp.smt2
+ regress0/proofs/issue277-circuit-propagator.smt2
+ regress0/proofs/lfsc-test-1.smt2
+ regress0/proofs/open-pf-datatypes.smt2
+ regress0/proofs/open-pf-if-unordered-iff.smt2
+ regress0/proofs/open-pf-rederivation.smt2
+ regress0/proofs/project-issue317-inc-sat-conflictlit.smt2
+ regress0/proofs/project-issue330-eqproof.smt2
+ regress0/proofs/proj-issue326-nl-bounds-check.smt2
+ regress0/proofs/proj-issue342-eager-checking-no-proof-checking.smt2
+ regress0/proofs/qgu-fuzz-1-bool-sat.smt2
+ regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2
+ regress0/proofs/qgu-fuzz-3-chainres-checking.smt2
+ regress0/proofs/qgu-fuzz-4-bool-chainres-postprocessing-singleton.smt2
+ regress0/proofs/qgu-fuzz-5-bool-open-sat.smt2
regress0/proofs/scope.smt2
+ regress0/proofs/trust-subs-eq-open.smt2
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_49.smt2
regress0/push-pop/boolean/fuzz_50.smt2
regress0/push-pop/bug1990.smt2
- regress0/push-pop/bug233.cvc
+ regress0/push-pop/bug233.cvc.smt2
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/incremental-subst-bug.cvc.smt2
regress0/push-pop/issue1986.smt2
regress0/push-pop/issue2137.min.smt2
+ regress0/push-pop/issue6535-inc-solve.smt2
+ regress0/push-pop/issue7479-global-decls.smt2
regress0/push-pop/quant-fun-proc-unfd.smt2
regress0/push-pop/real-as-int-incremental.smt2
regress0/push-pop/simple_unsat_cores.smt2
- regress0/push-pop/test.00.cvc
- regress0/push-pop/test.01.cvc
+ regress0/push-pop/test.00.cvc.smt2
+ regress0/push-pop/test.01.cvc.smt2
regress0/push-pop/tiny_bug.smt2
- regress0/push-pop/units.cvc
+ regress0/push-pop/units.cvc.smt2
regress0/quantifiers/agg-rew-test-cf.smt2
regress0/quantifiers/agg-rew-test.smt2
regress0/quantifiers/ari056.smt2
regress0/quantifiers/bug749-rounding.smt2
regress0/quantifiers/cbqi-lia-dt-simp.smt2
regress0/quantifiers/cegqi-needs-justify.smt2
- regress0/quantifiers/cegqi-nl-simp.cvc
+ regress0/quantifiers/cegqi-nl-simp.cvc.smt2
regress0/quantifiers/cegqi-nl-sq.smt2
regress0/quantifiers/cegqi-par-dt-simple.smt2
regress0/quantifiers/clock-10.smt2
regress0/quantifiers/issue4576.smt2
regress0/quantifiers/issue5645-dt-cm-spurious.smt2
regress0/quantifiers/issue5693-prenex.smt2
+ regress0/quantifiers/issue6475-rr-const.smt2
+ regress0/quantifiers/issue6603-dt-bool-cegqi.smt2
+ regress0/quantifiers/issue6838-qpdt.smt2
+ regress0/quantifiers/issue6996-trivial-elim.smt2
+ regress0/quantifiers/issue6999-deq-elim.smt2
+ regress0/quantifiers/issue7353-var-elim-par-dt.smt2
regress0/quantifiers/lra-triv-gn.smt2
regress0/quantifiers/macro-back-subs-sat.smt2
regress0/quantifiers/macros-int-real.smt2
regress0/quantifiers/simp-len.smt2
regress0/quantifiers/simp-typ-test.smt2
regress0/quantifiers/ufnia-fv-delta.smt2
+ regress0/quantifiers/veqt-delta.smt2
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_1.cvc
- regress0/rels/rel_join_0.cvc
- regress0/rels/rel_join_1_1.cvc
- regress0/rels/rel_join_1.cvc
- regress0/rels/rel_join_2_1.cvc
- regress0/rels/rel_join_2.cvc
- regress0/rels/rel_join_3_1.cvc
- regress0/rels/rel_join_3.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_1.cvc
- regress0/rels/rel_product_0.cvc
- regress0/rels/rel_product_1_1.cvc
- regress0/rels/rel_product_1.cvc
- regress0/rels/rel_symbolic_1_1.cvc
- regress0/rels/rel_symbolic_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_1.cvc
- regress0/rels/rel_tc_3.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_1.cvc
- regress0/rels/rel_transpose_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/addr_book_0.cvc.smt2
+ regress0/rels/atom_univ2.cvc.smt2
+ regress0/rels/card_transpose.cvc.smt2
+ regress0/rels/iden_0.cvc.smt2
+ regress0/rels/iden_1.cvc.smt2
+ regress0/rels/join-eq-u-sat.cvc.smt2
+ regress0/rels/join-eq-u.cvc.smt2
+ regress0/rels/joinImg_0.cvc.smt2
+ regress0/rels/oneLoc_no_quant-int_0_1.cvc.smt2
+ regress0/rels/qgu-fuzz-relations-1.smt2
+ regress0/rels/qgu-fuzz-relations-1-dd.smt2
+ regress0/rels/rel_1tup_0.cvc.smt2
+ regress0/rels/rel_complex_0.cvc.smt2
+ regress0/rels/rel_complex_1.cvc.smt2
+ regress0/rels/rel_conflict_0.cvc.smt2
+ regress0/rels/rel_join_0_1.cvc.smt2
+ regress0/rels/rel_join_0.cvc.smt2
+ regress0/rels/rel_join_1_1.cvc.smt2
+ regress0/rels/rel_join_1.cvc.smt2
+ regress0/rels/rel_join_2_1.cvc.smt2
+ regress0/rels/rel_join_2.cvc.smt2
+ regress0/rels/rel_join_3_1.cvc.smt2
+ regress0/rels/rel_join_3.cvc.smt2
+ regress0/rels/rel_join_4.cvc.smt2
+ regress0/rels/rel_join_5.cvc.smt2
+ regress0/rels/rel_join_6.cvc.smt2
+ regress0/rels/rel_join_7.cvc.smt2
+ regress0/rels/rel_product_0_1.cvc.smt2
+ regress0/rels/rel_product_0.cvc.smt2
+ regress0/rels/rel_product_1_1.cvc.smt2
+ regress0/rels/rel_product_1.cvc.smt2
+ regress0/rels/rel_symbolic_1_1.cvc.smt2
+ regress0/rels/rel_symbolic_1.cvc.smt2
+ regress0/rels/rel_symbolic_2_1.cvc.smt2
+ regress0/rels/rel_symbolic_3_1.cvc.smt2
+ regress0/rels/rel_tc_11.cvc.smt2
+ regress0/rels/rel_tc_2_1.cvc.smt2
+ regress0/rels/rel_tc_3_1.cvc.smt2
+ regress0/rels/rel_tc_3.cvc.smt2
+ regress0/rels/rel_tc_8.cvc.smt2
+ regress0/rels/rel_tp_3_1.cvc.smt2
+ regress0/rels/rel_tp_join_0.cvc.smt2
+ regress0/rels/rel_tp_join_1.cvc.smt2
+ regress0/rels/rel_tp_join_2.cvc.smt2
+ regress0/rels/rel_tp_join_3.cvc.smt2
+ regress0/rels/rel_tp_join_eq_0.cvc.smt2
+ regress0/rels/rel_tp_join_int_0.cvc.smt2
+ regress0/rels/rel_tp_join_pro_0.cvc.smt2
+ regress0/rels/rel_tp_join_var_0.cvc.smt2
+ regress0/rels/rel_transpose_0.cvc.smt2
+ regress0/rels/rel_transpose_1_1.cvc.smt2
+ regress0/rels/rel_transpose_1.cvc.smt2
+ regress0/rels/rel_transpose_3.cvc.smt2
+ regress0/rels/rel_transpose_4.cvc.smt2
+ regress0/rels/rel_transpose_5.cvc.smt2
+ regress0/rels/rel_transpose_6.cvc.smt2
+ regress0/rels/rel_transpose_7.cvc.smt2
regress0/rels/relations-ops.smt2
- regress0/rels/rels-sharing-simp.cvc
+ regress0/rels/rels-sharing-simp.cvc.smt2
regress0/sep/dispose-1.smt2
regress0/sep/dup-nemp.smt2
regress0/sep/issue3720-check-model.smt2
regress0/seq/issue5543-unit-cmv.smt2
regress0/seq/issue5547-seq-len-unit.smt2
regress0/seq/issue5547-small-seq-len-unit.smt2
+ regress0/seq/issue5665-invalid-model.smt2
+ regress0/seq/issue6337-seq.smt2
regress0/seq/len_simplify.smt2
+ regress0/seq/proj-issue340.smt2
regress0/seq/seq-2var.smt2
regress0/seq/seq-ex1.smt2
regress0/seq/seq-ex2.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-3sets.cvc.smt2
regress0/sets/card.smt2
regress0/sets/card3-ground.smt2
regress0/sets/comp-qf-error.smt2
- regress0/sets/complement.cvc
- regress0/sets/complement2.cvc
- regress0/sets/complement3.cvc
- regress0/sets/cvc-sample.cvc
+ regress0/sets/complement.cvc.smt2
+ regress0/sets/complement2.cvc.smt2
+ regress0/sets/complement3.cvc.smt2
+ regress0/sets/cvc-sample.cvc.smt2
regress0/sets/dt-simp-mem.smt2
regress0/sets/emptyset.smt2
regress0/sets/eqtest.smt2
regress0/sets/pre-proc-univ.smt2
regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
regress0/sets/setel-eq.smt2
+ regress0/sets/sets-deq-dd.smt2
regress0/sets/sets-equal.smt2
regress0/sets/sets-extr.smt2
regress0/sets/sets-inter.smt2
regress0/simple-rdl.smtv1.smt2
regress0/simple-uf.smt2
regress0/simple-uf.smtv1.smt2
- regress0/simple.cvc
+ regress0/simple.cvc.smt2
regress0/simple.smtv1.smt2
regress0/simple2.smtv1.smt2
regress0/simplification_bug.smtv1.smt2
regress0/simplification_bug2.smtv1.smt2
- regress0/smallcnf.cvc
+ regress0/smallcnf.cvc.smt2
regress0/smt2output.smt2
regress0/smtlib/define-fun-rec-logic.smt2
regress0/smtlib/get-unsat-assumptions.smt2
regress0/strings/code-perf.smt2
regress0/strings/code-sat-neg-one.smt2
regress0/strings/complement-simple.smt2
+ regress0/strings/delta-trust-subs.smt2
regress0/strings/escchar_25.smt2
regress0/strings/escchar.smt2
regress0/strings/from_code.smt2
regress0/strings/idof-sem.smt2
regress0/strings/ilc-like.smt2
regress0/strings/indexof-sym-simp.smt2
+ regress0/strings/indexof_re.smt2
+ regress0/strings/indexof_re-start-index.smt2
regress0/strings/is_digit_simple.smt2
regress0/strings/issue1189.smt2
regress0/strings/issue2958.smt2
regress0/strings/issue5090.smt2
regress0/strings/issue5384-double-conflict.smt2
regress0/strings/issue5428-re-diff-assoc.smt2
+ regress0/strings/issue5508-multiple-conflicts.smt2
regress0/strings/issue5542-strings-seq-mix.smt2
regress0/strings/issue5608-eager-pp.smt2
regress0/strings/issue5666-orig-unit-deq.smt2
regress0/strings/issue5816-re-kind.smt2
regress0/strings/issue5915-repl-ctn-rewrite.smt2
regress0/strings/issue6203-3-unfold-trivial-true.smt2
+ regress0/strings/issue6510-seq-bool.smt2
+ regress0/strings/issue6520.smt2
+ regress0/strings/issue6560-indexof-reduction.smt2
+ regress0/strings/issue6604-re-elim.smt2
+ regress0/strings/issue6643-ctn-decompose-conflict.smt2
+ regress0/strings/issue6681-split-eq-strip-l.smt2
+ regress0/strings/issue6834-str-eq-const-nhomog.smt2
regress0/strings/itos-entail.smt2
regress0/strings/large-model.smt2
regress0/strings/leadingzero001.smt2
regress0/strings/ncontrib-rewrites.smt2
regress0/strings/norn-31.smt2
regress0/strings/norn-simp-rew.smt2
- regress0/strings/parser-syms.cvc
- regress0/strings/quad-028-2-2-unsat.smt2
+ regress0/strings/parser-syms.cvc.smt2
+ regress0/strings/proj-issue316-regexp-ite.smt2
regress0/strings/re_diff.smt2
regress0/strings/re-in-rewrite.smt2
regress0/strings/re-syntax.smt2
regress0/strings/re.all.smt2
regress0/strings/regexp_inclusion_reduction.smt2
regress0/strings/regexp_inclusion.smt2
- regress0/strings/regexp-native-simple.cvc
+ regress0/strings/regexp-native-simple.cvc.smt2
regress0/strings/repl-rewrites2.smt2
regress0/strings/replace-const.smt2
regress0/strings/replaceall-eval.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/strings-charat.cvc.smt2
+ regress0/strings/strings-native-simple.cvc.smt2
regress0/strings/strip-endpoint-itos.smt2
regress0/strings/substr-rewrites.smt2
regress0/strings/tolower-rrs.smt2
regress0/strings/unicode-esc.smt2
regress0/strings/unsound-0908.smt2
regress0/strings/unsound-repl-rewrite.smt2
+ regress0/sygus/assume-simple.sy
regress0/sygus/array-grammar-select.sy
regress0/sygus/ccp16.lus.sy
regress0/sygus/cegqi-si-string-triv-2fun.sy
regress0/sygus/dt-sel-parse1.sy
regress0/sygus/General_plus10.sy
regress0/sygus/hd-05-d1-prog-nogrammar.sy
+ regress0/sygus/ho-occ-synth-fun.sy
regress0/sygus/inv-different-var-order.sy
regress0/sygus/issue3356-syg-inf-usort.smt2
regress0/sygus/issue3624.sy
regress0/sygus/pLTL-sygus-syntax-err.sy
regress0/sygus/print-debug.sy
regress0/sygus/print-define-fun.sy
+ regress0/sygus/print-grammar.sy
regress0/sygus/real-si-all.sy
+ regress0/sygus/setFeature.sy
regress0/sygus/strings-unconstrained.sy
regress0/sygus/sygus-no-wf.sy
regress0/sygus/sygus-uf.sy
regress0/sygus/uminus_one.sy
regress0/sygus/univ_3-long-repeat-conflict.sy
regress0/symmetric.smtv1.smt2
- regress0/test11.cvc
- regress0/test9.cvc
+ regress0/test11.cvc.smt2
+ regress0/test9.cvc.smt2
regress0/tptp/ARI086=1.p
regress0/tptp/DAT001=1.p
regress0/tptp/is_rat_simple.p
regress0/uf/NEQ016_size5_reduced2b.smtv1.smt2
regress0/uf/pred.smtv1.smt2
regress0/uf/SEQ032_size2.smtv1.smt2
- 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/uf/simple.01.cvc.smt2
+ regress0/uf/simple.02.cvc.smt2
+ regress0/uf/simple.03.cvc.smt2
+ regress0/uf/simple.04.cvc.smt2
+ regress0/uf20-03.cvc.smt2
regress0/uflia/check01.smt2
regress0/uflia/check02.smt2
regress0/uflia/check03.smt2
regress0/uflia/xs-09-16-3-4-1-5.delta03.smtv1.smt2
regress0/uflia/xs-09-16-3-4-1-5.delta04.smtv1.smt2
regress0/uflia/xs-09-16-3-4-1-5.delta05.smtv1.smt2
- regress0/uflra/bug293.cvc
+ regress0/uflra/bug293.cvc.smt2
regress0/uflra/bug449.smtv1.smt2
regress0/uflra/constants0.smtv1.smt2
regress0/uflra/fuzz01.smtv1.smt2
regress0/uflra/pb_real_10_0200_10_26.smtv1.smt2
regress0/uflra/pb_real_10_0200_10_27.smtv1.smt2
regress0/uflra/pb_real_10_0200_10_29.smtv1.smt2
- regress0/uflra/simple.01.cvc
- regress0/uflra/simple.02.cvc
- regress0/uflra/simple.03.cvc
- regress0/uflra/simple.04.cvc
+ regress0/uflra/simple.01.cvc.smt2
+ regress0/uflra/simple.02.cvc.smt2
+ regress0/uflra/simple.03.cvc.smt2
+ regress0/uflra/simple.04.cvc.smt2
regress0/unconstrained/4481.smt2
regress0/unconstrained/arith.smt2
regress0/unconstrained/arith2.smt2
regress0/unconstrained/geq.smt2
regress0/unconstrained/gt.smt2
regress0/unconstrained/issue4644.smt2
+ regress0/unconstrained/issue4656-bool-term-vars.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/use_approx/bug812_approx.smt2
+ regress0/use_approx/error0_approx.smt2
+ regress0/use_approx/issue2429_approx.smt2
+ regress0/use_approx/issue4714_approx.smt2
+ regress0/use_approx/siegel-nl-bases_approx.smt2
+ regress0/use_approx/specsharp-WindowsCard.15.RTE.Terminate_System.Int32_approx.smt2
+ regress0/wiki.01.cvc.smt2
+ regress0/wiki.02.cvc.smt2
+ regress0/wiki.03.cvc.smt2
+ regress0/wiki.04.cvc.smt2
+ regress0/wiki.05.cvc.smt2
+ regress0/wiki.06.cvc.smt2
+ regress0/wiki.07.cvc.smt2
+ regress0/wiki.08.cvc.smt2
+ regress0/wiki.09.cvc.smt2
+ regress0/wiki.10.cvc.smt2
+ regress0/wiki.11.cvc.smt2
+ regress0/wiki.12.cvc.smt2
+ regress0/wiki.13.cvc.smt2
+ regress0/wiki.14.cvc.smt2
+ regress0/wiki.15.cvc.smt2
+ regress0/wiki.16.cvc.smt2
+ regress0/wiki.17.cvc.smt2
+ regress0/wiki.18.cvc.smt2
+ regress0/wiki.19.cvc.smt2
+ regress0/wiki.20.cvc.smt2
+ regress0/wiki.21.cvc.smt2
)
#-----------------------------------------------------------------------------#
# Regression level 1 tests
set(regress_1_tests
- regress1/abduct-dt.smt2
+ regress1/abduction/abd-real-const.smt2
+ regress1/abduction/sygus-abduct-test-user.smt2
+ regress1/abduction/issue5848-4.smt2
+ regress1/abduction/issue5848-2.smt2
+ regress1/abduction/issue5848.smt2
+ regress1/abduction/issue6605-1.smt2
+ regress1/abduction/abduct-dt.smt2
+ regress1/abduction/sygus-abduct-test-ccore.smt2
+ regress1/abduction/sygus-abduct-test.smt2
+ regress1/abduction/abd-simple-conj-4.smt2
+ regress1/abduction/abduction_streq.readable.smt2
+ regress1/abduction/yoni-true-sol.smt2
+ regress1/abduction/uf-abduct.smt2
+ regress1/abduction/abduction_1255.corecstrs.readable.smt2
+ regress1/abduction/abduction-no-pbe-sym-break.smt2
+ regress1/abduction/issue5848-3-trivial-no-abduct.smt2
+ regress1/abduction/sygus-abduct-ex1-grammar.smt2
regress1/arith/arith-brab-test.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/arith-int-004.cvc.smt2
+ regress1/arith/arith-int-011.cvc.smt2
+ regress1/arith/arith-int-012.cvc.smt2
+ regress1/arith/arith-int-013.cvc.smt2
+ regress1/arith/arith-int-022.cvc.smt2
+ regress1/arith/arith-int-024.cvc.smt2
+ regress1/arith/arith-int-047.cvc.smt2
+ regress1/arith/arith-int-048.cvc.smt2
+ regress1/arith/arith-int-050.cvc.smt2
+ regress1/arith/arith-int-084.cvc.smt2
+ regress1/arith/arith-int-085.cvc.smt2
+ regress1/arith/arith-int-097.cvc.smt2
regress1/arith/bug547.1.smt2
regress1/arith/bug716.0.smt2
- regress1/arith/bug716.1.cvc
- regress1/arith/bug716.2.cvc
+ regress1/arith/bug716.1.cvc.smt2
+ regress1/arith/bug716.2.cvc.smt2
regress1/arith/div.03.smt2
regress1/arith/div.06.smt2
regress1/arith/div.08.smt2
regress1/arith/issue3952-rew-eq.smt2
regress1/arith/issue4985-model-success.smt2
regress1/arith/issue4985b-model-success.smt2
+ regress1/arith/issue6774-sanity-int-model.smt2
+ regress1/arith/issue7252-arith-sanity.smt2
regress1/arith/issue789.smt2
- regress1/arith/miplib3.cvc
+ regress1/arith/miplib3.cvc.smt2
regress1/arith/mod.02.smt2
regress1/arith/mod.03.smt2
regress1/arith/mult.02.smt2
regress1/aufbv/fuzz10.smtv1.smt2
regress1/auflia/bug330.smt2
regress1/boolean-terms-kernel2.smt2
- regress1/boolean.cvc
+ regress1/boolean.cvc.smt2
regress1/bug296.smt2
- regress1/bug425.cvc
+ regress1/bug425.cvc.smt2
regress1/bug507.smt2
regress1/bug512.smt2
regress1/bug516.smt2
regress1/bug681.smt2
regress1/bug694-Unapply1.scala-0.smt2
regress1/bug800.smt2
+ regress1/bags/card1.smt2
+ regress1/bags/choose1.smt2
+ regress1/bags/choose2.smt2
+ regress1/bags/choose3.smt2
+ regress1/bags/choose4.smt2
regress1/bags/difference_remove1.smt2
regress1/bags/disequality.smt2
regress1/bags/duplicate_removal1.smt2
regress1/bags/duplicate_removal2.smt2
regress1/bags/emptybag1.smt2
+ regress1/bags/fold1.smt2
+ regress1/bags/fuzzy1.smt2
+ regress1/bags/fuzzy2.smt2
+ regress1/bags/fuzzy3.smt2
+ regress1/bags/fuzzy4.smt2
+ regress1/bags/fuzzy5.smt2
+ regress1/bags/fuzzy6.smt2
regress1/bags/intersection_min1.smt2
regress1/bags/intersection_min2.smt2
regress1/bags/issue5759.smt2
+ regress1/bags/map-lazy-lam.smt2
+ regress1/bags/map1.smt2
+ regress1/bags/map2.smt2
+ regress1/bags/map3.smt2
regress1/bags/subbag1.smt2
regress1/bags/subbag2.smt2
regress1/bags/union_disjoint.smt2
regress1/bags/union_max1.smt2
regress1/bags/union_max2.smt2
+ regress1/bv2int-isabelle.smt2
regress1/bv/bench_38.delta.smt2
regress1/bv/bug787.smt2
regress1/bv/bug_extract_mult_leading_bit.smt2
regress1/bv/incorrect1.smtv1.smt2
regress1/bv/issue3654.smt2
regress1/bv/issue3776.smt2
+ regress1/bv/issue3958.smt2
regress1/bv/min-pp-rewrite-error.smt2
- regress1/bv/test-bv-abstraction.smt2
regress1/bv/unsound1.smt2
regress1/bvdiv2.smt2
- regress1/constarr3.cvc
+ regress1/cee-bug0909-dd-scope.smt2
+ regress1/constarr3.cvc.smt2
regress1/constarr3.smt2
+ regress1/cores/issue5604.smt2
+ regress1/cores/issue6988-arith-sanity.smt2
regress1/datatypes/acyclicity-sr-ground096.smt2
+ regress1/datatypes/cee-prs-small-dd2.smt2
regress1/datatypes/dt-color-2.6.smt2
regress1/datatypes/dt-param-card4-unsat.smt2
- regress1/datatypes/error.cvc
regress1/datatypes/issue3266-small.smt2
+ regress1/datatypes/issue4851-cdt-model.smt2
regress1/datatypes/issue-variant-dt-zero.smt2
regress1/datatypes/manos-model.smt2
regress1/datatypes/non-simple-rec.smt2
regress1/datatypes/tuple_projection.smt2
regress1/decision/bug374a.smtv1.smt2
regress1/decision/error3.smtv1.smt2
+ regress1/decision/issue5454-2.smt2
+ regress1/decision/issue5454-3.smt2
+ regress1/decision/issue5454.smt2
+ regress1/decision/issue5785.smt2
+ regress1/decision/jh-test1.smt2
regress1/decision/quant-Arrays_Q1-noinfer.smt2
- regress1/error.cvc
+ regress1/decision/wishue114.smt2
+ regress1/decision/wishue115.smt2
+ regress1/decision/wishue116.smt2
+ regress1/decision/wishue149-2.smt2
+ regress1/decision/wishue149-3.smt2
+ regress1/decision/wishue160.smt2
regress1/errorcrash.smt2
+ regress1/fp/fp_to_real.smt2
regress1/fp/rti_3_5_bug_report.smt2
regress1/fmf-fun-dbu.smt2
regress1/fmf/ALG008-1.smt2
regress1/fmf/agree466.smt2
regress1/fmf/agree467.smt2
regress1/fmf/alg202+1.smt2
- regress1/fmf/am-bad-model.cvc
+ regress1/fmf/am-bad-model.cvc.smt2
regress1/fmf/bound-int-alt.smt2
regress1/fmf/bug0909.smt2
regress1/fmf/bug651.smt2
regress1/fmf/issue4068-si-qf.smt2
regress1/fmf/issue4225-univ-fun.smt2
regress1/fmf/issue5738-dt-interp-finite.smt2
+ regress1/fmf/issue6690-re-enum.smt2
+ regress1/fmf/issue6744-2-unc-bool-var.smt2
+ regress1/fmf/issue6744-3-unc-bool-var.smt2
regress1/fmf/issue916-fmf-or.smt2
regress1/fmf/jasmin-cdt-crash.smt2
+ regress1/fmf/ko-bound-set.cvc.smt2
regress1/fmf/loopy_coda.smt2
regress1/fmf/lst-no-self-rev-exp.smt2
- regress1/fmf/memory_model-R_cpp-dd.cvc
+ regress1/fmf/memory_model-R_cpp-dd.cvc.smt2
regress1/fmf/nlp042+1.smt2
regress1/fmf/nun-0208-to.smt2
regress1/fmf/pow2-bool.smt2
regress1/fmf/sort-inf-int.smt2
regress1/fmf/with-ind-104-core.smt2
regress1/gensys_brn001.smt2
- regress1/ho/bug_freevar_PHI004^4-delta.smt2
regress1/ho/bug_freeVar_BDD_General_data_270.p
+ regress1/ho/bug_freevar_PHI004^4-delta.smt2
regress1/ho/bound_var_bug.p
regress1/ho/fta0328.lfho.p
+ regress1/ho/ho-fun-sharing-dd.smt2
regress1/ho/issue3136-fconst-bool-bool.smt2
regress1/ho/issue4065-no-rep.smt2
regress1/ho/issue4092-sinf.smt2
regress1/ho/issue4134-sinf.smt2
- regress1/ho/nested_lambdas-AGT034^2.smt2
- regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
+ regress1/ho/issue4758.smt2
+ regress1/ho/issue5078-small.smt2
+ regress1/ho/issue5201-1.smt2
+ regress1/ho/issue5741-3.smt2
regress1/ho/NUM638^1.smt2
regress1/ho/NUM925^1.p
regress1/ho/soundness_fmf_SYO362^5-delta.p
regress1/ho/store-ax-min.p
- regress1/ho/SYO056^1.p
- regress1/hole6.cvc
+ regress1/hole6.cvc.smt2
regress1/ite5.smt2
regress1/issue3970-nl-ext-purify.smt2
regress1/issue3990-sort-inference.smt2
regress1/issue5739-rtf-processed.smt2
regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2
regress1/lemmas/pursuit-safety-8.smtv1.smt2
- regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
+ regress1/minimal_unsat_core.smt2
regress1/model-blocker-simple.smt2
regress1/model-blocker-values.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/exp_monotone.smt2
regress1/nl/ext-rew-aggr-test.smt2
regress1/nl/factor_agg_s.smt2
- regress1/nl/iand-native-1.smt2
regress1/nl/iand-native-2.smt2
regress1/nl/iand-native-granularities.smt2
regress1/nl/issue3300-approx-sqrt-witness.smt2
regress1/nl/issue3656.smt2
regress1/nl/issue3803-nl-check-model.smt2
regress1/nl/issue3955-ee-double-notify.smt2
+ regress1/nl/issue3966-conf-coeff.smt2
+ regress1/nl/issue4791-llr.smt2
regress1/nl/issue5372-2-no-m-presolve.smt2
+ regress1/nl/issue5660-mb-success.smt2
regress1/nl/issue5662-nl-tc.smt2
regress1/nl/issue5662-nl-tc-min.smt2
regress1/nl/metitarski-1025.smt2
regress1/nl/nl-help-unsat-quant.smt2
regress1/nl/nl-unk-quant.smt2
regress1/nl/nl_uf_lalt.smt2
+ regress1/nl/nra-cad-performance.smt2
regress1/nl/ones.smt2
regress1/nl/pinto-model-core-ni.smt2
regress1/nl/poly-1025.smt2
+ regress1/nl/proj-365-is-int-pi.smt2
regress1/nl/quant-nl.smt2
regress1/nl/red-exp.smt2
regress1/nl/rewriting-sums.smt2
regress1/nl/sugar-ident-3.smt2
regress1/nl/sugar-ident.smt2
regress1/nl/tan-rewrite2.smt2
- regress1/nl/ufnia-factor-open-proof.smt2
regress1/nl/zero-subset.smt2
regress1/non-fatal-errors.smt2
- regress1/parsing_ringer.cvc
regress1/proof00.smt2
+ regress1/proofs/issue6625-unsat-core-proofs.smt2
regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2
regress1/proofs/macro-res-exp-singleton-after-elimCrowd.smt2
+ regress1/proofs/qgu-fuzz-1-strings-pp.smt2
+ regress1/proofs/qgu-fuzz-arrays-1-dd-te-auto.smt2
+ regress1/proofs/quant-alpha-eq.smt2
regress1/proofs/sat-trivial-cycle.smt2
+ regress1/proofs/str-ovf-dd.smt2
+ regress1/proofs/unsat-cores-proofs.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/cee-prs-small.smt2
regress1/push-pop/fuzz_1.smt2
regress1/push-pop/fuzz_10.smt2
regress1/push-pop/fuzz_11.smt2
regress1/push-pop/fuzz_7.smt2
regress1/push-pop/fuzz_8.smt2
regress1/push-pop/fuzz_9.smt2
+ regress1/push-pop/issue6773-arith-no-check.smt2
regress1/push-pop/model-unsound-ania.smt2
regress1/push-pop/quant-fun-proc-unmacro.smt2
regress1/push-pop/quant-fun-proc.smt2
regress1/quantifiers/burns13.smt2
regress1/quantifiers/burns4.smt2
regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2
+ regress1/quantifiers/cee-npnt-dd.smt2
+ regress1/quantifiers/cee-os-delta.smt2
regress1/quantifiers/cdt-0208-to.smt2
- regress1/quantifiers/const.cvc
- regress1/quantifiers/constfunc.cvc
+ regress1/quantifiers/choice-move-delta-relt.smt2
+ regress1/quantifiers/const.cvc.smt2
+ regress1/quantifiers/constfunc.cvc.smt2
+ regress1/quantifiers/ddatv-delta2.smt2
regress1/quantifiers/dt-tc-opt-small.smt2
regress1/quantifiers/dump-inst-i.smt2
regress1/quantifiers/dump-inst-proof.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/issue3316.smt2
regress1/quantifiers/issue3317.smt2
regress1/quantifiers/issue3481.smt2
- regress1/quantifiers/issue3481-unsat1.smt2
regress1/quantifiers/issue3537.smt2
regress1/quantifiers/issue3628.smt2
regress1/quantifiers/issue3664.smt2
regress1/quantifiers/issue4433-nqe.smt2
regress1/quantifiers/issue4620-erq-witness-unsound.smt2
regress1/quantifiers/issue4685-wrewrite.smt2
+ regress1/quantifiers/issue4813-qe-quant.smt2
regress1/quantifiers/issue4849-nqe.smt2
regress1/quantifiers/issue5019-cegqi-i.smt2
+ regress1/quantifiers/issue5278-ext-rewrite-rec.smt2
regress1/quantifiers/issue5279-nqe.smt2
+ regress1/quantifiers/issue5288-vts-real-int.smt2
regress1/quantifiers/issue5365-nqe.smt2
regress1/quantifiers/issue5378-witness.smt2
regress1/quantifiers/issue5469-aext.smt2
regress1/quantifiers/issue5506-qe.smt2
regress1/quantifiers/issue5507-qe.smt2
regress1/quantifiers/issue5658-qe.smt2
+ regress1/quantifiers/issue5735-subtypes.smt2
+ regress1/quantifiers/issue5735-2-subtypes.smt2
regress1/quantifiers/issue5766-wrong-sel-trigger.smt2
regress1/quantifiers/issue5899-qe.smt2
+ regress1/quantifiers/issue6607-witness-te.smt2
+ regress1/quantifiers/issue6638-sygus-inst.smt2
+ regress1/quantifiers/issue6642-em-types.smt2
+ regress1/quantifiers/issue6699-nc-shadow.smt2
+ regress1/quantifiers/issue6775-vts-int.smt2
+ regress1/quantifiers/issue6845-nl-lemma-tc.smt2
+ regress1/quantifiers/issue7385-sygus-inst-i.smt2
+ regress1/quantifiers/issue7537-cegqi-comp-types.smt2
regress1/quantifiers/issue993.smt2
regress1/quantifiers/javafe.ast.StmtVec.009.smt2
regress1/quantifiers/lia-witness-div-pp.smt2
regress1/quantifiers/min-ppgt-em-incomplete.smt2
regress1/quantifiers/min-ppgt-em-incomplete2.smt2
regress1/quantifiers/mix-coeff.smt2
- regress1/quantifiers/mutualrec2.cvc
+ regress1/quantifiers/mutualrec2.cvc.smt2
regress1/quantifiers/nested9_true-unreach-call.i_575.smt2
regress1/quantifiers/nl-pow-trick.smt2
regress1/quantifiers/nra-interleave-inst.smt2
regress1/quantifiers/quant-wf-int-ind.smt2
regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2
regress1/quantifiers/qs-has-term.smt2
- regress1/quantifiers/recfact.cvc
+ regress1/quantifiers/recfact.cvc.smt2
+ regress1/quantifiers/rel-trigger-unusable.smt2
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/set-choice-koikonomou.cvc.smt2
+ regress1/quantifiers/set3.smt2
regress1/quantifiers/set8.smt2
regress1/quantifiers/seu169+1.smt2
regress1/quantifiers/seq-solved-enum.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/sygus-inst-nia-psyco-060.smt2
- regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2
regress1/quantifiers/symmetric_unsat_7.smt2
regress1/quantifiers/tpp-unit-fail-qbv.smt2
regress1/quantifiers/var-eq-trigger.smt2
regress1/quantifiers/var-eq-trigger-simple.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/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/addr_book_1.cvc.smt2
+ regress1/rels/addr_book_1_1.cvc.smt2
+ regress1/rels/bv1-unit.cvc.smt2
+ regress1/rels/bv1-unitb.cvc.smt2
+ regress1/rels/bv1.cvc.smt2
+ regress1/rels/bv1p-sat.cvc.smt2
+ regress1/rels/bv1p.cvc.smt2
+ regress1/rels/bv2.cvc.smt2
+ regress1/rels/iden_1_1.cvc.smt2
+ regress1/rels/join-eq-structure-and.cvc.smt2
+ regress1/rels/join-eq-structure.cvc.smt2
+ regress1/rels/joinImg_0_1.cvc.smt2
+ regress1/rels/joinImg_0_2.cvc.smt2
+ regress1/rels/joinImg_1.cvc.smt2
+ regress1/rels/joinImg_1_1.cvc.smt2
+ regress1/rels/joinImg_2.cvc.smt2
+ regress1/rels/joinImg_2_1.cvc.smt2
+ regress1/rels/prod-mod-eq.cvc.smt2
+ regress1/rels/prod-mod-eq2.cvc.smt2
+ regress1/rels/qgu-fuzz-relations-2.smt2
+ regress1/rels/qgu-fuzz-relations-3-upwards.smt2
+ regress1/rels/rel_complex_3.cvc.smt2
+ regress1/rels/rel_complex_4.cvc.smt2
+ regress1/rels/rel_complex_5.cvc.smt2
+ regress1/rels/rel_mix_0_1.cvc.smt2
+ regress1/rels/rel_pressure_0.cvc.smt2
+ regress1/rels/rel_tc_10_1.cvc.smt2
+ regress1/rels/rel_tc_4.cvc.smt2
+ regress1/rels/rel_tc_4_1.cvc.smt2
+ regress1/rels/rel_tc_5_1.cvc.smt2
+ regress1/rels/rel_tc_6.cvc.smt2
+ regress1/rels/rel_tc_9_1.cvc.smt2
+ regress1/rels/rel_tp_2.cvc.smt2
+ regress1/rels/rel_tp_join_2_1.cvc.smt2
+ regress1/rels/set-strat.cvc.smt2
+ regress1/rels/strat.cvc.smt2
regress1/rr-verify/bool-crci.sy
regress1/rr-verify/bv-term-32.sy
regress1/rr-verify/bv-term.sy
regress1/sep/wand-simp-sat.smt2
regress1/sep/wand-simp-sat2.smt2
regress1/sep/wand-simp-unsat.smt2
- regress1/sets/choose.cvc
+ regress1/sets/choose.cvc.smt2
regress1/sets/choose1.smt2
regress1/sets/choose2.smt2
regress1/sets/choose3.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/arjun-set-univ.cvc.smt2
regress1/sets/card-3.smt2
regress1/sets/card-4.smt2
regress1/sets/card-5.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/sets-tuple-poly.cvc.smt2
+ regress1/sets/sets-uc-wrong.smt2
regress1/sets/set-comp-sat.smt2
regress1/sets/sharingbug.smt2
regress1/sets/univ-set-uf-elim.smt2
regress1/strings/bug686dd.smt2
regress1/strings/bug768.smt2
regress1/strings/bug799-min.smt2
+ regress1/strings/cee-norn-aes-trivially.smt2
regress1/strings/chapman150408.smt2
regress1/strings/cmu-2db2-extf-reg.smt2
regress1/strings/cmu-5042-0707-2.smt2
regress1/strings/cmu-substr-rw.smt2
regress1/strings/code-sequence.smt2
regress1/strings/complement-test.smt2
+ regress1/strings/indexof_re_red.smt2
regress1/strings/crash-1019.smt2
regress1/strings/csp-prefix-exp-bug.smt2
regress1/strings/double-replace.smt2
regress1/strings/idof-neg-index.smt2
regress1/strings/idof-triv.smt2
regress1/strings/ilc-l-nt.smt2
+ regress1/strings/instance3303-delta.smt2
+ regress1/strings/instance7075-delta.smt2
regress1/strings/issue1105.smt2
regress1/strings/issue1684-regex.smt2
regress1/strings/issue2060.smt2
regress1/strings/issue5692-infer-proxy.smt2
regress1/strings/issue5940-skc-len-conc.smt2
regress1/strings/issue5940-2-skc-len-conc.smt2
+ regress1/strings/issue6057-replace-re.smt2
+ regress1/strings/issue6057-replace-re-all-jiwonparc.smt2
regress1/strings/issue6072-inc-no-const-reg.smt2
regress1/strings/issue6075-repl-len-one-rr.smt2
+ regress1/strings/issue6101.smt2
+ regress1/strings/issue6101-2.smt2
regress1/strings/issue6132-non-unique-skolem.smt2
regress1/strings/issue6142-repl-inv-rew.smt2
+ regress1/strings/issue6180-proxy-vars.smt2
+ regress1/strings/issue6180-2-proxy-vars.smt2
+ regress1/strings/issue6184-unsat-core.smt2
regress1/strings/issue6191-replace-all.smt2
regress1/strings/issue6203-1-substr-ctn-strip.smt2
regress1/strings/issue6203-2-re-ccache.smt2
+ regress1/strings/issue6203-6-replace-re.smt2
regress1/strings/issue6214-2-sym-re-inc.smt2
regress1/strings/issue6214-3-sym-re-inc.smt2
regress1/strings/issue6214-4-sym-re-inc.smt2
regress1/strings/issue6270.smt2
regress1/strings/issue6271-rnf.smt2
regress1/strings/issue6271-2-rnf.smt2
+ regress1/strings/issue6337-replace-re-all.smt2
+ regress1/strings/issue6337-replace-re.smt2
+ regress1/strings/issue6567-empty-re-range.smt2
+ regress1/strings/issue6604-2.smt2
+ regress1/strings/issue6635-rre.smt2
+ regress1/strings/issue6653-2-update-c-len.smt2
+ regress1/strings/issue6653-3-seq.smt2
+ regress1/strings/issue6653-4-rre.smt2
+ regress1/strings/issue6653-rre.smt2
+ regress1/strings/issue6653-rre-small.smt2
+ regress1/strings/issue6766-re-elim-bv.smt2
+ regress1/strings/issue6777-seq-nth-eval-cm.smt2
+ regress1/strings/issue6913.smt2
+ regress1/strings/issue6973-dup-lemma-conc.smt2
+ regress1/strings/issue7677-test-const-rv.smt2
regress1/strings/kaluza-fl.smt2
regress1/strings/loop002.smt2
regress1/strings/loop003.smt2
regress1/strings/nf-ff-contains-abs.smt2
regress1/strings/no-lazy-pp-quant.smt2
regress1/strings/non_termination_regular_expression4.smt2
+ regress1/strings/non-terminating-rewrite-aent.smt2
regress1/strings/norn-13.smt2
regress1/strings/norn-360.smt2
regress1/strings/norn-ab.smt2
regress1/strings/norn-simp-rew-sat.smt2
regress1/strings/nt6-dd.smt2
regress1/strings/nterm-re-inter-sigma.smt2
+ regress1/strings/open-pf-merge.smt2
+ regress1/strings/pattern1.smt2
regress1/strings/pierre150331.smt2
regress1/strings/policy_variable.smt2
regress1/strings/pre_ctn_no_skolem_share.smt2
+ regress1/strings/proj254-re-elim-agg.smt2
+ regress1/strings/proj-issue331.smt2
regress1/strings/query4674.smt2
regress1/strings/query8485.smt2
regress1/strings/re-all-char-hard.smt2
regress1/strings/rev-ex5.smt2
regress1/strings/rew-020618.smt2
regress1/strings/rew-check1.smt2
+ regress1/strings/seq-cardinality.smt2
+ regress1/strings/seq-quant-infinite-branch.smt2
regress1/strings/simple-re-consume.smt2
regress1/strings/stoi-400million.smt2
regress1/strings/stoi-solve.smt2
regress1/strings/update-ex1.smt2
regress1/strings/update-ex2.smt2
regress1/strings/username_checker_min.smt2
- regress1/sygus-abduct-ex1-grammar.smt2
- regress1/sygus-abduct-test.smt2
- regress1/sygus-abduct-test-ccore.smt2
- regress1/sygus-abduct-test-user.smt2
regress1/sygus/VC22_a.sy
- regress1/sygus/abd-simple-conj-4.smt2
- regress1/sygus/abduction_1255.corecstrs.readable.smt2
- regress1/sygus/abduction_streq.readable.smt2
regress1/sygus/abv.sy
regress1/sygus/array-grammar-store.sy
regress1/sygus/array_search_5-Q-easy.sy
+ regress1/sygus/array-uc.sy
regress1/sygus/bvudiv-by-2.sy
regress1/sygus/cegar1.sy
regress1/sygus/cegis-unif-inv-eq-fair.sy
regress1/sygus/interpol_from_pono_2.smt2
regress1/sygus/issue2914.sy
regress1/sygus/issue2935.sy
+ regress1/sygus/issue3109-share-sel.sy
regress1/sygus/issue3199.smt2
regress1/sygus/issue3200.smt2
regress1/sygus/issue3201.smt2
regress1/sygus/issue3634.smt2
regress1/sygus/issue3635.smt2
regress1/sygus/issue3644.smt2
- regress1/sygus/issue3648.smt2
regress1/sygus/issue3649.sy
regress1/sygus/issue3802-default-consts.sy
regress1/sygus/issue3839-cond-rewrite.smt2
regress1/sygus/re-concat.sy
regress1/sygus/repair-const-rl.sy
regress1/sygus/replicate-mod.sy
+ regress1/sygus/replicate-mod-assume.sy
regress1/sygus/rex-strings-alarm.sy
regress1/sygus/sets-pred-test.sy
regress1/sygus/simple-regexp.sy
regress1/sygus/trivial-stream.sy
regress1/sygus/twolets1.sy
regress1/sygus/twolets2-orig.sy
- regress1/sygus/uf-abduct.smt2
regress1/sygus/unbdd_inv_gen_winf1.sy
regress1/sygus/univ_2-long-repeat.sy
- regress1/sygus/yoni-true-sol.smt2
regress1/sym/q-constant.smt2
regress1/sym/q-function.smt2
regress1/sym/qf-function.smt2
regress1/sym/sym5.smt2
regress1/sym/sym6.smt2
regress1/sym/sym7-uf.smt2
- regress1/test12.cvc
- regress1/trim.cvc
+ regress1/test12.cvc.smt2
+ regress1/trim.cvc.smt2
regress1/uf2.smt2
regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2
regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2
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.smtv1.smt2
- regress2/arith/arith-int-098.cvc
+ regress2/arith/arith-int-098.cvc.smt2
regress2/arith/pursuit-safety-11.smtv1.smt2
regress2/arith/pursuit-safety-12.smtv1.smt2
regress2/arith/real2int-test.smt2
regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
regress2/bv_to_int_bvmul1.smt2
regress2/bv_to_int_inc1.smt2
- regress2/bv_to_int_mask_array_1.smt2
regress2/bv_to_int_mask_array_2.smt2
regress2/bv_to_int_mask_array_3.smt2
regress2/bv_to_int_shifts.smt2
- regress2/error0.smt2
regress2/error1.smtv1.smt2
+ regress2/fp/issue7056.smt2
regress2/fuzz_2.smtv1.smt2
regress2/hash_sat_06_19.smt2
regress2/hash_sat_07_17.smt2
regress2/ho/fta0409.smt2
regress2/ho/involved_parsing_ALG248^3.p
regress2/ho/partial_app_interpreted_SWW474^2.p
- regress2/ho/SYO362^5.p
- regress2/hole7.cvc
- regress2/hole8.cvc
+ regress2/hole7.cvc.smt2
+ regress2/hole8.cvc.smt2
regress2/instance_1444.smtv1.smt2
regress2/issue3687-check-models.smt2
regress2/issue4707-bv-to-bool-large.smt2
+ regress2/issue6495-dup-pat-term.smt2
+ regress2/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2
regress2/javafe.ast.WhileStmt.447_no_forall.smt2
- regress2/nl/nt-lemmas-bad.smt2
+ regress2/nl/ufnia-factor-open-proof.smt2
regress2/ooo.rf6.smt2
regress2/ooo.tag10.smt2
regress2/piVC_5581bd.smt2
+ regress2/proofs/sat-proof-reloaded-reason.smt2
regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2
regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2
- regress2/quantifiers/ForElimination-scala-9.smt2
+ regress2/quantifiers/cee-event-wrong-sat.smt2
+ regress2/quantifiers/exp-trivially-dd3.smt2
regress2/quantifiers/gn-wrong-091018.smt2
- regress2/quantifiers/javafe.ast.ArrayInit.35.smt2
+ regress2/quantifiers/issue3481-unsat1.smt2
regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2
regress2/quantifiers/javafe.ast.WhileStmt.447.smt2
regress2/quantifiers/javafe.tc.CheckCompilationUnit.001.smt2
regress2/strings/cmu-repl-len-nterm.smt2
regress2/strings/issue3203.smt2
regress2/strings/issue5381.smt2
+ regress2/strings/issue6483.smt2
+ regress2/strings/issue6057-replace-re-all.smt2
+ regress2/strings/issue6057-replace-re-all-simplified.smt2
+ regress2/strings/issue6636-replace-re-all.smt2
+ regress2/strings/issue6637-replace-re-all.smt2
+ regress2/strings/issue6639-replace-re-all.smt2
regress2/strings/issue918.smt2
regress2/strings/non_termination_regular_expression6.smt2
+ regress2/strings/proof-fail-083021-delta.smt2
regress2/strings/range-perf.smt2
regress2/strings/repl-repl-i-no-push.smt2
regress2/strings/repl-repl.smt2
regress2/strings/replaceall-diffrange.smt2
regress2/strings/replaceall-len-c.smt2
regress2/strings/small-1.smt2
+ regress2/strings/strings-alpha-card-129.smt2
regress2/strings/update-ex3.smt2
regress2/strings/update-ex4-seq.smt2
regress2/sygus/MPwL_d1s3.sy
regress2/sygus/pbe_bvurem.sy
regress2/sygus/process-10-vars-2fun.sy
regress2/sygus/process-arg-invariance.sy
+ regress2/sygus/qgu-bools.sy
regress2/sygus/real-grammar-neg.sy
regress2/sygus/sets-fun-test.sy
+ regress2/sygus/sumn_recur_synth.sy
regress2/sygus/strings-no-syntax-len.sy
regress2/sygus/three.sy
- regress2/typed_v1l50016-simp.cvc
+ regress2/typed_v1l50016-simp.cvc.smt2
regress2/uflia-error0.smt2
regress2/xs-09-16-3-4-1-5.smtv1.smt2
)
# Regression level 3 tests
set(regress_3_tests
+ regress3/arith/abz5_1400.smtv1.smt2
regress3/arith_prp-13-24.smt2
regress3/aufbv-wchains010ue.smtv1.smt2
regress3/auflia-fuzz06.smtv1.smt2
regress3/decision-wchains010ue.smtv1.smt2
regress3/DRAGON_1.lus.sy
regress3/eq_diamond14.smtv1.smt2
+ regress3/error0.smt2
regress3/friedman_n4_i5.smtv1.smt2
regress3/friedman_n6_i4.smtv1.smt2
- regress3/hole9.cvc
- regress3/hole10.cvc
+ regress3/ho/SYO362^5.p
+ regress3/hole9.cvc.smt2
+ regress3/hole10.cvc.smt2
regress3/incorrect1.smtv1.smt2
regress3/interpol2.smt2
regress3/inv_gen_n_c11.sy
regress3/issue4170.smt2
- regress3/issue4476-ext-rew.smt2
regress3/issue4714.smt2
regress3/lpsat-goal-9.smt2
regress3/nia-max-square.sy
+ regress3/nl/iand-native-1.smt2
regress3/PEQ018_size4.smtv1.smt2
regress3/policyM.sy
+ regress3/quantifiers/ForElimination-scala-9.smt2
+ regress3/quantifiers/javafe.ast.ArrayInit.35.smt2
regress3/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2
regress3/qwh.35.405.shuffled-as.sat03-1651.smtv1.smt2
regress3/regex-rrv.sy
- regress3/siegel-nl-bases.smt2
regress3/sixfuncs.sy
regress3/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2
regress3/strings-any-term.sy
regress3/strings/extf_d_perf.smt2
+ regress3/strings/indexof_re_red.smt2
regress3/strings/norn-dis-0707-3.smt2
regress3/strings/replace_re_all.smt2
regress3/unbdd_inv_gen_ex7.sy
- regress3/unifpi-solve-car_1.lus.sy
regress3/vcb.sy
)
regress4/NEQ016_size5.smtv1.smt2
regress4/pp-regfile.smtv1.smt2
regress4/sets-card-neg-mem-union-2.smt2
+ regress4/siegel-nl-bases.smt2
regress4/unsat-circ-reduce.smt2
regress4/xs-11-20-5-2-5-3.smt2
regress4/xs-11-20-5-2-5-3.smtv1.smt2
regress0/auflia/fuzz01.smtv1.smt2
###
regress0/bv/test00.smtv1.smt2
+ # timeout after fixing upwards closure for relations
+ regress0/rels/rel_tc_7.cvc.smt2
+ # timeout after changes to equality rewriting policy in strings
+ regress0/strings/quad-028-2-2-unsat.smt2
# FIXME #1649
- regress0/datatypes/datatype-dump.cvc
+ regress0/datatypes/datatype-dump.cvc.smt2
# no longer support overloaded symbols across multiple parametric datatypes
regress0/datatypes/repeated-selectors-2769.smt2
# need finite model finding command line in tptp regression
regress0/tptp/SYN075+1.p
regress0/uf/iso_icl_repgen004.smtv1.smt2
###
+ # takes around 30 sec
+ regress1/bags/fold2.smt2
regress1/bug472.smt2
regress1/datatypes/non-simple-rec-set.smt2
- # TODO: fix models (projects #276)
- regress1/fmf/ko-bound-set.cvc
# results in an assertion failure (see issue #1650).
regress1/ho/hoa0102.smt2
- # slow on some builds after changes to tangent planes
- regress1/nl/approx-sqrt-unsat.smt2
+ # after disallowing solving for terms with quantifiers
+ regress1/ho/nested_lambdas-AGT034^2.smt2
+ regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
+ regress1/ho/SYO056^1.p
# times out after update to circuit propagator
regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2
# times out after update to tangent planes
regress1/quantifiers/anti-sk-simp.smt2
# no longer support snorm option
regress1/quantifiers/arith-snorm.smt2
+ # timeout on some builds after changes to justification heuristic
+ regress1/quantifiers/infer-arith-trigger-eq.smt2
# ajreynol: different error messages on production and debug:
regress1/quantifiers/macro-subtype-param.smt2
# times out with competition build, ok with other builds:
regress1/quantifiers/model_6_1_bv.smt2
- # timeout after changes to nonlinear on PR #5351
- regress1/quantifiers/rel-trigger-unusable.smt2
- # does not terminate/takes a long time when doing a coverage build with LFSC.
- regress1/quantifiers/set3.smt2
- # changes to expand definitions, related to trigger selection for selectors
- regress1/quantifiers/stream-x2014-09-18-unsat.smt2
# ajreynol: different error messages on production and debug:
regress1/quantifiers/subtype-param-unk.smt2
regress1/quantifiers/subtype-param.smt2
+ # timeout after changes to theory preprocessing, note is non-linear and does not involve sygus-inst
+ regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2
###
- regress1/rels/garbage_collect.cvc
+ regress1/rels/garbage_collect.cvc.smt2
regress1/sets/setofsets-disequal.smt2
regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2
# no longer support quant-epr + sep
regress1/sygus/interpol_from_pono_3.smt2
regress1/sygus/interpol_dt.smt2
regress1/sygus/inv_gen_fig8.sy
+ # timeout since nl-rlv is required; however it cannot be used with quantifiers
+ regress1/sygus/issue3648.smt2
# new reconstruct algorithm is slow at reconstructing random constants (see wishue #82)
regress0/sygus/c100.sy
# For the six regressions below, solution terms require rewrites not in
# previously sygus inference did not apply, now (correctly) times out
regress1/sygus/issue3498.smt2
regress2/arith/miplib-opt1217--27.smt2
+ # times out after #7345
+ regress2/bv_to_int_mask_array_1.smt2
regress2/nl/dumortier-050317.smt2
+ # timeout on some builds after changes to justification heuristic
+ regress2/nl/nt-lemmas-bad.smt2
+ # timeout after refactoring justification heuristic
+ regress2/ho/SYO362^5.p
+ # time out
+ regress3/unifpi-solve-car_1.lus.sy
+ # unknown (is sat)
+ regress3/issue4476-ext-rew.smt2
)
#-----------------------------------------------------------------------------#
projects / cvc5.git / blobdiff