summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-06-14[LFSC] Fix memory leaksfix_eqproofAndres Noetzli
2017-05-26Fix EqProof memory managementAndres Noetzli
2017-05-26fixed most leaksAndres Noetzli
2017-05-26fixed most leaksAndres Noetzli
2017-05-24Fix use-after-free with ResChainsAndres Noetzli
This commit fixes an issue where the ResChain in `d_resolutionChains` gets deleted here: https://github.com/CVC4/CVC4/blob/master/src/proof/sat_proof_implementation.h#L729 The condition immediately after is false because the condition on line 727 is true. Thus, `d_resolutionChains` now has a deleted entry for `id`. When CVC4 afterwards gets the ResChain associated with `id` in `checkResolution()`, it accesses the deleted entry: https://github.com/CVC4/CVC4/blob/master/src/proof/sat_proof_implementation.h#L303
2017-05-22Initial draft of 2017 competition scripts.ajreynol
2017-05-20Fix bug 812.ajreynol
2017-05-17Merge pull request #155 from makaimann/conditional_coverageClark Barrett
Conditional coverage
2017-05-16Merge pull request #161 from 4tXJ7f/fix_parserClark Barrett
Avoid tokenizing FP tokens in non-FP input
2017-05-16Merge pull request #160 from 4tXJ7f/fix_win_buildClark Barrett
Fix error in Windows build
2017-05-16Avoid tokenizing FP tokens in non-FP inputAndres Noetzli
This commit addresses bug 807. CVC4 was parsing floating-point related tokens such as NaN as floating-point tokens even for inputs that do not use the FP theory, which lead to failing SMT-LIB benchmarks that declare functions named NaN.
2017-05-16Fix error in Windows buildAndres Noetzli
The Windows build was missing the `print_statistics()` function, this commit moves the function out of the `#ifndef __WIN32__` guard.
2017-05-15Merge pull request #156 from 4tXJ7f/fix_safe_printAndrew Reynolds
Minor fix in safe_print function
2017-05-15Minor fix in safe_print functionAndres Noetzli
This commit fixes two issues reported by Coverity: - Fixes the check whether the buffer is full in safe_print_hex - Removes dead code in safe_print for floating-point values Additionally, it fixes an issue reported by Andy where the names of the statistics were printed as "<unsupported>" due to calling the const char* version instead of the std::string version of safe_print. Finally, this fixes an issue where --segv-spin would not print the program name because it was a const char*. The program name is now stored as a string. NOTE: As a side effect, the last part also fixes Coverity issue 1362944, which has been in CVC4 for a long time.
2017-05-15Cleanup handling of division (possible fix for bugs 803, 804, 805).ajreynol
2017-05-15Merge pull request #159 from 4tXJ7f/fix_set_typesAndrew Reynolds
Fix type checks for relation operators
2017-05-15Fix type checks for relation operatorsAndres Noetzli
This commit fixes an assertion error when applying transpose or transitive closure to a set instead of a relation. Instead it now prints a parse error.
2017-05-15Merge pull request #158 from 4tXJ7f/fix_sets_rewriterAndrew Reynolds
Fix minor bug in sets rewriter
2017-05-15Fix minor bug in sets rewriterAndres Noetzli
As reported by Coverity, one of the switches in the sets rewriter had a missing break. This could lead to an assertion failure when rewriting the cardinality of a transpose as in the test case included in this commit.
2017-05-15Fix bug 806. Minor fixes to remove term formula pass.ajreynol
2017-05-15Merge pull request #157 from 4tXJ7f/fix_iteratorAndrew Reynolds
Fix condition in upwards closure check for sets
2017-05-15Fix condition in upwards closure check for setsAndres Noetzli
Coverity reported this mismatched iterator.
2017-05-15Fix issue in ceg_instantiator related to types and theoryOf, fixes bug 802.ajreynol
2017-05-15Make conflict-based instantiation abort if a ground conflict is found in the ↵ajreynol
master equality engine during term indexing, fixes bug 801.
2017-05-13Merge pull request #154 from 4tXJ7f/fix_testClark Barrett
Fix out-of-bounds access in test
2017-05-13Fix out-of-bounds access in testAndres Notzli
2017-05-12Adding VPATH back inmakaimann
2017-05-12Conditional coverage buildmakaimann
2017-05-12Make signal handlers saferAndres Notzli
As reported in bug 769, the signal handlers currently use unsafe functions such as dynamic memory allocations and fprintf. This commit fixes the issue by introducing functions for printing statistics in signal handlers (functions with the `safe` prefix). It also avoids copying statistics, which further avoids dynamic memory allocation. The safe printing of statistics has some limitations (it does not support SExprStats or printing CVC4::Result), which should not matter much in practice. Printing statistics in a non-signal handler is not affected by these changes as that uses a separate code path (the functions without the `safe` prefix). Additional changes: - Remove ListStat as it is not used anywhere - Add unit test for safe printing statistics
2017-05-10Do not split on cardinality for string equivalence classes with non-constant ↵ajreynol
lengths if disequalities already imply sufficient lower bound. Fixes bug 799.
2017-05-09Change str.replace for empty string.ajreynol
2017-05-05Do not eliminate extended arithmetic symbols when finite model finding is ↵ajreynol
on, add regression.
2017-05-05Fix error message.ajreynol
2017-05-04skolemization manager may be called also when just unsatCores are on ↵guykatzz
(related to bug 717)
2017-05-04fixing bug 790: track dependencies when the unsatCores() option is onguykatzz
2017-04-28Partial fix for bug 717.experimentClark Barrett
2017-04-28Minor fixesajreynol
2017-04-28Fix bug for real division.ajreynol
2017-04-28Do not eliminate non-standard arithmetic operators in recursive function ↵ajreynol
definitions, add regression.
2017-04-24Fixes and simplifications for fmf mbqi.ajreynol
2017-04-24Fix parsing selectors for nullary constructors in smtlib 2.6 format.ajreynol
2017-04-23Merge pull request #152 from ↵Andrew Reynolds
timothy-king/delta-rational-value-cases-second-submission Updating TheoryArithPrivate::getDeltaValue() to eagerly use the parti…
2017-04-23Changing spaces to tabs in Makefile.Tim King
2017-04-22Updating TheoryArithPrivate::getDeltaValue() to eagerly use the partial ↵Tim King
model value if exists.
2017-04-21Merge pull request #151 from 4tXJ7f/fix_debugClark Barrett
Move assertion out of loop for better performance
2017-04-21Disabled bug639.smt2 which still fails.Clark Barrett
2017-04-21Add test cases for bugs 639 and 681.Clark Barrett
2017-04-21Fix for bug 681 (now gives reasonable error message about using constantClark Barrett
arrays).
2017-04-21Move assertion out of loop for better performanceAndres 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-21Merge pull request #150 from 4tXJ7f/check_exceptions2Clark Barrett
Add check for C++ exceptions to config script
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback