git.libre-soc.org Git - cvc5.git/commit

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Sun, 25 Apr 2021 19:56:01 +0000 (14:56 -0500)
committer	GitHub <noreply@github.com>
	Sun, 25 Apr 2021 19:56:01 +0000 (14:56 -0500)
commit	dce2fd01164df92e66e94c5aee4f95491d3ab5d9
tree	d1e9f374d6f36bb90c2c7668bb62a1b45170d21e	tree
parent	8f50a5600e0664330128d2ac824092a685ef965e	commit \| diff

More check models (#6439)

107 files changed:

test/regress/regress0/arith/ackermann.real.smt2		diff \| blob \| history
test/regress/regress0/arith/integers/ackermann1.smt2		diff \| blob \| history
test/regress/regress0/arith/integers/ackermann2.smt2		diff \| blob \| history
test/regress/regress0/arith/integers/ackermann3.smt2		diff \| blob \| history
test/regress/regress0/arith/integers/ackermann4.smt2		diff \| blob \| history
test/regress/regress0/arith/integers/ackermann5.smt2		diff \| blob \| history
test/regress/regress0/arith/integers/ackermann6.smt2		diff \| blob \| history
test/regress/regress0/bv/ackermann2.smt2		diff \| blob \| history
test/regress/regress0/bv/ackermann3.smt2		diff \| blob \| history
test/regress/regress0/bv/ackermann5.smt2		diff \| blob \| history
test/regress/regress0/bv/ackermann6.smt2		diff \| blob \| history
test/regress/regress0/bv/ackermann7.smt2		diff \| blob \| history
test/regress/regress0/bv/ackermann8.smt2		diff \| blob \| history
test/regress/regress0/bv/bv-abstr-bug.smt2		diff \| blob \| history
test/regress/regress0/bv/int_to_bv_err_on_demand_1.smt2		diff \| blob \| history
test/regress/regress0/fmf/fd-false.smt2		diff \| blob \| history
test/regress/regress0/issue4010-sort-inf-var.smt2		diff \| blob \| history
test/regress/regress0/issue4469-unc-no-reuse-var.smt2		diff \| blob \| history
test/regress/regress0/nl/issue3003.smt2		diff \| blob \| history
test/regress/regress0/nl/issue3407.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/delta-simp.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/mix-complete-strat.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/mix-simp.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/pure_dt_cbqi.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/arith.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/arith2.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/arith3.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/arith4.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/arith5.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/arith6.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/arith7.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/array1.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvbool.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvbool2.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvbool3.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvcmp.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvconcat.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvconcat2.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvdiv.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvext.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvite.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvmul.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvmul2.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvmul3.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvnot.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvsle.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvsle2.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvsle3.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvsle4.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvsle5.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvslt.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvslt2.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvslt3.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvslt4.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvslt5.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvule.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvule2.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvule3.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvule4.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvule5.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvult.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvult2.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvult3.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvult4.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/bvult5.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/geq.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/gt.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/ite.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/leq.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/lt.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/mult1.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/uf1.smt2		diff \| blob \| history
test/regress/regress0/unconstrained/xor.smt2		diff \| blob \| history
test/regress/regress1/bug519.smt2		diff \| blob \| history
test/regress/regress1/datatypes/issue-variant-dt-zero.smt2		diff \| blob \| history
test/regress/regress1/fmf/ALG008-1.smt2		diff \| blob \| history
test/regress/regress1/fmf/issue4068-si-qf.smt2		diff \| blob \| history
test/regress/regress1/fmf/nlp042+1.smt2		diff \| blob \| history
test/regress/regress1/fmf/pow2-bool.smt2		diff \| blob \| history
test/regress/regress1/fmf/sort-inf-int-real.smt2		diff \| blob \| history
test/regress/regress1/fmf/sort-inf-int.smt2		diff \| blob \| history
test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2		diff \| blob \| history
test/regress/regress1/ho/issue4092-sinf.smt2		diff \| blob \| history
test/regress/regress1/ho/issue4134-sinf.smt2		diff \| blob \| history
test/regress/regress1/nl/factor_agg_s.smt2		diff \| blob \| history
test/regress/regress1/nl/iand-native-1.smt2		diff \| blob \| history
test/regress/regress1/nl/iand-native-granularities.smt2		diff \| blob \| history
test/regress/regress1/nl/issue3307.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/RND-small.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/issue3316.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/issue3537.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/issue3765-quant-dd.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/psyco-196.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/small-pipeline-fixpoint-3.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/sygus-infer-nested.smt2		diff \| blob \| history
test/regress/regress1/sep/finite-witness-sat.smt2		diff \| blob \| history
test/regress/regress1/sep/sep-fmf-priority.smt2		diff \| blob \| history
test/regress/regress1/sep/split-find-unsat.smt2		diff \| blob \| history
test/regress/regress1/sep/wand-simp-unsat.smt2		diff \| blob \| history
test/regress/regress1/sets/choose.cvc		diff \| blob \| history
test/regress/regress1/sqrt2-sort-inf-unk.smt2		diff \| blob \| history
test/regress/regress1/sygus/issue3498.smt2		diff \| blob \| history
test/regress/regress1/sygus/issue3514.smt2		diff \| blob \| history
test/regress/regress1/sygus/issue3644.smt2		diff \| blob \| history
test/regress/regress2/quantifiers/gn-wrong-091018.smt2		diff \| blob \| history
test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2		diff \| blob \| history

RSS Atom