More check models (#6439)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 25 Apr 2021 19:56:01 +0000 (14:56 -0500)
committerGitHub <noreply@github.com>
Sun, 25 Apr 2021 19:56:01 +0000 (14:56 -0500)
commitdce2fd01164df92e66e94c5aee4f95491d3ab5d9
treed1e9f374d6f36bb90c2c7668bb62a1b45170d21e
parent8f50a5600e0664330128d2ac824092a685ef965e
More check models (#6439)
107 files changed:
test/regress/regress0/arith/ackermann.real.smt2
test/regress/regress0/arith/integers/ackermann1.smt2
test/regress/regress0/arith/integers/ackermann2.smt2
test/regress/regress0/arith/integers/ackermann3.smt2
test/regress/regress0/arith/integers/ackermann4.smt2
test/regress/regress0/arith/integers/ackermann5.smt2
test/regress/regress0/arith/integers/ackermann6.smt2
test/regress/regress0/bv/ackermann2.smt2
test/regress/regress0/bv/ackermann3.smt2
test/regress/regress0/bv/ackermann5.smt2
test/regress/regress0/bv/ackermann6.smt2
test/regress/regress0/bv/ackermann7.smt2
test/regress/regress0/bv/ackermann8.smt2
test/regress/regress0/bv/bv-abstr-bug.smt2
test/regress/regress0/bv/int_to_bv_err_on_demand_1.smt2
test/regress/regress0/fmf/fd-false.smt2
test/regress/regress0/issue4010-sort-inf-var.smt2
test/regress/regress0/issue4469-unc-no-reuse-var.smt2
test/regress/regress0/nl/issue3003.smt2
test/regress/regress0/nl/issue3407.smt2
test/regress/regress0/quantifiers/delta-simp.smt2
test/regress/regress0/quantifiers/mix-complete-strat.smt2
test/regress/regress0/quantifiers/mix-simp.smt2
test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
test/regress/regress0/unconstrained/arith.smt2
test/regress/regress0/unconstrained/arith2.smt2
test/regress/regress0/unconstrained/arith3.smt2
test/regress/regress0/unconstrained/arith4.smt2
test/regress/regress0/unconstrained/arith5.smt2
test/regress/regress0/unconstrained/arith6.smt2
test/regress/regress0/unconstrained/arith7.smt2
test/regress/regress0/unconstrained/array1.smt2
test/regress/regress0/unconstrained/bvbool.smt2
test/regress/regress0/unconstrained/bvbool2.smt2
test/regress/regress0/unconstrained/bvbool3.smt2
test/regress/regress0/unconstrained/bvcmp.smt2
test/regress/regress0/unconstrained/bvconcat.smt2
test/regress/regress0/unconstrained/bvconcat2.smt2
test/regress/regress0/unconstrained/bvdiv.smt2
test/regress/regress0/unconstrained/bvext.smt2
test/regress/regress0/unconstrained/bvite.smt2
test/regress/regress0/unconstrained/bvmul.smt2
test/regress/regress0/unconstrained/bvmul2.smt2
test/regress/regress0/unconstrained/bvmul3.smt2
test/regress/regress0/unconstrained/bvnot.smt2
test/regress/regress0/unconstrained/bvsle.smt2
test/regress/regress0/unconstrained/bvsle2.smt2
test/regress/regress0/unconstrained/bvsle3.smt2
test/regress/regress0/unconstrained/bvsle4.smt2
test/regress/regress0/unconstrained/bvsle5.smt2
test/regress/regress0/unconstrained/bvslt.smt2
test/regress/regress0/unconstrained/bvslt2.smt2
test/regress/regress0/unconstrained/bvslt3.smt2
test/regress/regress0/unconstrained/bvslt4.smt2
test/regress/regress0/unconstrained/bvslt5.smt2
test/regress/regress0/unconstrained/bvule.smt2
test/regress/regress0/unconstrained/bvule2.smt2
test/regress/regress0/unconstrained/bvule3.smt2
test/regress/regress0/unconstrained/bvule4.smt2
test/regress/regress0/unconstrained/bvule5.smt2
test/regress/regress0/unconstrained/bvult.smt2
test/regress/regress0/unconstrained/bvult2.smt2
test/regress/regress0/unconstrained/bvult3.smt2
test/regress/regress0/unconstrained/bvult4.smt2
test/regress/regress0/unconstrained/bvult5.smt2
test/regress/regress0/unconstrained/geq.smt2
test/regress/regress0/unconstrained/gt.smt2
test/regress/regress0/unconstrained/ite.smt2
test/regress/regress0/unconstrained/leq.smt2
test/regress/regress0/unconstrained/lt.smt2
test/regress/regress0/unconstrained/mult1.smt2
test/regress/regress0/unconstrained/uf1.smt2
test/regress/regress0/unconstrained/xor.smt2
test/regress/regress1/bug519.smt2
test/regress/regress1/datatypes/issue-variant-dt-zero.smt2
test/regress/regress1/fmf/ALG008-1.smt2
test/regress/regress1/fmf/issue4068-si-qf.smt2
test/regress/regress1/fmf/nlp042+1.smt2
test/regress/regress1/fmf/pow2-bool.smt2
test/regress/regress1/fmf/sort-inf-int-real.smt2
test/regress/regress1/fmf/sort-inf-int.smt2
test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2
test/regress/regress1/ho/issue4092-sinf.smt2
test/regress/regress1/ho/issue4134-sinf.smt2
test/regress/regress1/nl/factor_agg_s.smt2
test/regress/regress1/nl/iand-native-1.smt2
test/regress/regress1/nl/iand-native-granularities.smt2
test/regress/regress1/nl/issue3307.smt2
test/regress/regress1/quantifiers/RND-small.smt2
test/regress/regress1/quantifiers/issue3316.smt2
test/regress/regress1/quantifiers/issue3537.smt2
test/regress/regress1/quantifiers/issue3765-quant-dd.smt2
test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2
test/regress/regress1/quantifiers/psyco-196.smt2
test/regress/regress1/quantifiers/small-pipeline-fixpoint-3.smt2
test/regress/regress1/quantifiers/sygus-infer-nested.smt2
test/regress/regress1/sep/finite-witness-sat.smt2
test/regress/regress1/sep/sep-fmf-priority.smt2
test/regress/regress1/sep/split-find-unsat.smt2
test/regress/regress1/sep/wand-simp-unsat.smt2
test/regress/regress1/sets/choose.cvc
test/regress/regress1/sqrt2-sort-inf-unk.smt2
test/regress/regress1/sygus/issue3498.smt2
test/regress/regress1/sygus/issue3514.smt2
test/regress/regress1/sygus/issue3644.smt2
test/regress/regress2/quantifiers/gn-wrong-091018.smt2
test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2