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

Age	Commit message (Collapse)	Author
2017-05-05	Do not eliminate extended arithmetic symbols when finite model finding is ↵	ajreynol
	on, add regression.
2017-05-05	Fix error message.	ajreynol

2017-05-04	skolemization manager may be called also when just unsatCores are on ↵	guykatzz
	(related to bug 717)
2017-05-04	fixing bug 790: track dependencies when the unsatCores() option is on	guykatzz

2017-04-28	Partial fix for bug 717.experiment	Clark Barrett

2017-04-28	Minor fixes	ajreynol

2017-04-28	Fix bug for real division.	ajreynol

2017-04-28	Do not eliminate non-standard arithmetic operators in recursive function ↵	ajreynol
	definitions, add regression.
2017-04-24	Fixes and simplifications for fmf mbqi.	ajreynol

2017-04-24	Fix parsing selectors for nullary constructors in smtlib 2.6 format.	ajreynol

2017-04-23	Merge pull request #152 from ↵	Andrew Reynolds
	timothy-king/delta-rational-value-cases-second-submission Updating TheoryArithPrivate::getDeltaValue() to eagerly use the parti…
2017-04-23	Changing spaces to tabs in Makefile.	Tim King

2017-04-22	Updating TheoryArithPrivate::getDeltaValue() to eagerly use the partial ↵	Tim King
	model value if exists.
2017-04-21	Merge pull request #151 from 4tXJ7f/fix_debug	Clark Barrett
	Move assertion out of loop for better performance
2017-04-21	Disabled bug639.smt2 which still fails.	Clark Barrett

2017-04-21	Add test cases for bugs 639 and 681.	Clark Barrett

2017-04-21	Fix for bug 681 (now gives reasonable error message about using constant	Clark Barrett
	arrays).
2017-04-21	Move assertion out of loop for better performance	Andres Noetzli
	This is related to bug 508. The debug build was taking much longer than the production build to compute the result. The issue was an assertion in a loop in nonClausalSimplify(). By moving the assertion outside of the loop, the debug build is now roughly an order of magnitude slower than the production build (instead of two orders of magnitude), which seems to be roughly in line with the difference for other benchmarks: Debug version before change: - Bug (minified version): 1065.6s - regress3/friedman_n6_i4.smt: 6.9s - regress2/uflia-error0.smt2: 6.3s - regress2/fuzz_2.smt: 2.3s Debug version after change: - Bug (minified version): 131.4s - regress3/friedman_n6_i4.smt: 6.7s - regress2/uflia-error0.smt2: 6.2s - regress2/fuzz_2.smt: 1.9s Production version: - Bug (minified version): 18.8s - regress3/friedman_n6_i4.smt: 0.8s - regress2/uflia-error0.smt2: 0.8s - regress2/fuzz_2.smt: 0.2s
2017-04-21	Merge pull request #150 from 4tXJ7f/check_exceptions2	Clark Barrett
	Add check for C++ exceptions to config script
2017-04-21	Fix new relations regressions to use sets-ext.	ajreynol

2017-04-21	Handle subtypes in sets. Bug fixes for tuples with subtypes.	ajreynol

2017-04-21	Add check for C++ exceptions to config script	Andres Notzli
	Bug 687 was caused by the configuration not properly supporting C++ exceptions. To avoid such an incidence in the future, this commit adds a simple check to `configure.ac` (when not cross compiling).
2017-04-20	Merge pull request #149 from PaulMeng/master	Andrew Reynolds
	Support for relational operators identity and join image
2017-04-20	Minor fixes.	ajreynol

2017-04-20	Support for relational operators identity and join image	Paul Meng

2017-04-19	Fix mktheoryrewriter and mktheorytraits for nullaryoperator.	ajreynol

2017-04-19	Fixes for handling set universe: restrict upwards rule for universe to ↵	ajreynol
	memberships into variable sets, do not variable eliminate sets during ppAssert.
2017-04-18	Merge pull request #147 from makaimann/coverage_fix	Clark Barrett
	Coverage fix
2017-04-18	Fix for bug 639.	Clark Barrett

2017-04-18	Coverage fix	makaimann
	Forcing some make variables to be absolute paths lcov does not (officially) support relative paths src/expr and src/options in particular were breaking it
2017-04-14	Actively split for upwards closusure intersection. Minor clean up, add ↵	ajreynol
	regressions.
2017-04-14	Fix bug related to portfolio with nullary operators.	ajreynol

2017-04-14	Fix nullary operator printers, minor.	ajreynol

2017-04-14	Fix for fmf-fun when the option is set by user command.	ajreynol

2017-04-13	Fix for some compilers	Clark Barrett

2017-04-12	Add nullary operator metakind.	ajreynol

2017-04-11	Bug fix in conjecture generation for --quant-ind.	ajreynol

2017-04-07	Change option names for nl.	ajreynol

2017-04-05	Merge pull request #143 from FabianWolff/master	Clark Barrett
	Fix several spelling errors
2017-04-05	Fix bug 698.	ajreynol

2017-04-05	Fixes for nlAlgSolveSubs.	ajreynol

2017-04-05	Merge pull request #145 from 4tXJ7f/fix_lfsc_args	Andrew Reynolds
	[LFSC] Fix segfault
2017-04-05	Caching for fun def process, add regression.	ajreynol

2017-04-05	[LFSC] Fix segfault	Andres Notzli
	LFSC did not detect when the number of arguments provided to a side condition did not match the expected number of arguments, which could lead to out-of-bounds reads and writes. This commit adds a check and fixes one of the proof rules that provided the wrong number of arguments.
2017-04-05	Remove extraneous portion of an nl regression.	ajreynol

2017-04-05	Add non-linear regressions, disable nlAlgSubs, do not do rep checking for ↵	ajreynol
	NONLINEAR_MULT terms. Ensure shared terms have correct model values in non-linear solver.
2017-04-05	Fix several spelling errors	Fabian Wolff

2017-04-04	Enable multi-trigger-linear by default, add option.	ajreynol

2017-04-04	Simplify Theory::collectModelInfo interface to not take deprecated fullModel ↵	ajreynol
	argument.
2017-04-04	Do not solve for 0-ary non-constant symbols (for which isVar returns true), ↵	ajreynol
	add regressions.