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

author	Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
	Mon, 24 Jan 2022 18:34:14 +0000 (12:34 -0600)
committer	GitHub <noreply@github.com>
	Mon, 24 Jan 2022 18:34:14 +0000 (18:34 +0000)
commit	d0bab2e969c3557596516f3460eede4f28e468a1
tree	8610659600bb44deb8d9f2c504ad30c5cc01235a	tree
parent	f0014b7ed0f810cba313aafde9236571625d2927	commit \| diff

Enable dump tester. (#7884)

This PR enables the dump tester, a parse-print-parse test for cvc5, on CI. It also includes some changes that reduce the number of regressions that fail with this tester.

30 files changed:

.github/workflows/ci.yml		diff \| blob \| history
src/main/command_executor.cpp		diff \| blob \| history
src/main/driver_unified.cpp		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
test/regress/regress0/bv/issue-4075.smt2		diff \| blob \| history
test/regress/regress0/bv/issue-4130.smt2		diff \| blob \| history
test/regress/regress0/datatypes/datatype-dump.cvc.smt2		diff \| blob \| history
test/regress/regress0/fp/issue-5524.smt2		diff \| blob \| history
test/regress/regress0/ho/issue4477.smt2		diff \| blob \| history
test/regress/regress0/issue1063-overloading-dt-cons.smt2		diff \| blob \| history
test/regress/regress0/options/didyoumean.smt2		diff \| blob \| history
test/regress/regress0/options/help.smt2		diff \| blob \| history
test/regress/regress0/options/named_muted.smt2		diff \| blob \| history
test/regress/regress0/parser/bv_nat.smt2		diff \| blob \| history
test/regress/regress0/parser/force_logic_set_logic.smt2		diff \| blob \| history
test/regress/regress0/parser/issue6908-get-value-uc.smt2		diff \| blob \| history
test/regress/regress0/parser/linear_arithmetic_err1.smt2		diff \| blob \| history
test/regress/regress0/parser/linear_arithmetic_err2.smt2		diff \| blob \| history
test/regress/regress0/parser/linear_arithmetic_err3.smt2		diff \| blob \| history
test/regress/regress0/parser/named-attr-error.smt2		diff \| blob \| history
test/regress/regress0/parser/shadow_fun_symbol_all.smt2		diff \| blob \| history
test/regress/regress0/parser/shadow_fun_symbol_nirat.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/issue4437-unc-quant.smt2		diff \| blob \| history
test/regress/regress0/sygus/issue5512-vvv.sy		diff \| blob \| history
test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy		diff \| blob \| history
test/regress/regress1/arrayinuf_error.smt2		diff \| blob \| history
test/regress/regress1/errorcrash.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2		diff \| blob \| history
test/regress/run_regression.py		diff \| blob \| history

RSS Atom