Age | Commit message (Collapse) | Author |
|
|
|
https://www.starexec.org/starexec/secure/details/job.jsp?id=6972
The plot is bit misleading. Those not on x=y, are from QF_BV/asp which are segfaulting (see bugzilla 623). No performance impact on other logics it was tested on.
|
|
|
|
delta lemmas.
|
|
|
|
|
|
simplification.
|
|
|
|
|
|
|
|
and strings preprocessing. Minor fix for conjecture generation for finite types.
|
|
|
|
|
|
utilities more robust. Fix bug in conjecture generation for non-parameterized operators.
|
|
id was used as an internal marker in a set of theories tagging reasons of a
propagated disequalities. Replaced it with THEORY_LAST which is not completely
kosher but is safe in the context being used.
|
|
|
|
change const are triggers from false to true in equality engines
Performance comparison:
https://www.starexec.org/starexec/secure/details/job.jsp?id=6941
Bug opened for testcase that became much worse:
http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=621
|
|
fun-def. Add skolemization options.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
signature. Add regressions.
|
|
|
|
|
|
This reverts commit d2b44175c45a6d2c2fa9c3f8ec1ca1c433cb399b.
|
|
regressions.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.
|
|
|
|
Making sure the CVC4 flags do not get overwritten after being set.
|
|
|
|
refactoring.
|