id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
42	CVC3 prover problems	zirkel	ywei	"Two problems:

1) For the factorial example, CVC3 prover returns unknown.  However, giving the same query to CVC3 at the command line works.  This should be checked to see if the API returns a different result than the interactive interface.  Also, someone should check to see if there's a bug in the way the query is passed to CVC3.

2) The prover class should just return false if CVC3 cannot prove valid or invalid.  It does not need to throw an exception."	defect	closed	major		symbolic	1.0	fixed	prover, cvc3, cvc, factorial, query