Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
Conditional coverage
|
|
Avoid tokenizing FP tokens in non-FP input
|
|
Fix error in Windows build
|
|
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.
|
|
The Windows build was missing the `print_statistics()` function, this commit
moves the function out of the `#ifndef __WIN32__` guard.
|
|
Minor fix in safe_print function
|
|
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.
|
|
|
|
Fix type checks for relation operators
|
|
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.
|
|
Fix minor bug in sets rewriter
|
|
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.
|
|
|
|
Fix condition in upwards closure check for sets
|
|
Coverity reported this mismatched iterator.
|
|
|
|
master equality engine during term indexing, fixes bug 801.
|
|
Fix out-of-bounds access in test
|
|
|
|
|
|
|
|
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
|
|
lengths if disequalities already imply sufficient lower bound. Fixes bug 799.
|
|
|
|
on, add regression.
|
|
|
|
(related to bug 717)
|
|
|
|
|
|
|
|
|
|
definitions, add regression.
|
|
|
|
|
|
timothy-king/delta-rational-value-cases-second-submission
Updating TheoryArithPrivate::getDeltaValue() to eagerly use the parti…
|
|
|
|
model value if exists.
|
|
Move assertion out of loop for better performance
|
|
|
|
|
|
arrays).
|
|
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
|
|
Add check for C++ exceptions to config script
|