cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2019-09-06	Remove SMT1 parser. (#3228)	Mathias Preiner
	This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version). Fixes #2948 and fixes #1313.
2019-08-04	Fix regression script for incremental SMT-LIB v2 benchmarks. (#3155)	Mathias Preiner
	The regression script did not extract the expected status from incremental SMT-LIB v2 benchmarks correctly if status was given via (set-info :status ...). The script used re.search for finding the status, which only searches for the first occurrence instead of finding all (set-info :status ...). This commit fixes the issue by using re.findall instead.
2010-02-04	assign expected-status to regressions	Morgan Deters

2010-02-04	Moved regressions into various levels based on running time.	Tim King