| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
integers (default schema).
|
|
|
|
|
|
|
|
Conflicts:
test/regress/regress0/Makefile.am
|
|
This reverts commit a8e0ce673ba00533a663804cf74500e4d9a3a5cb.
|
|
setting inst-level 0 only for input terms.
|
|
Code changed but comment didn't, might as well get rid of it.
|
|
--enable-static-binary.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
modules check (introduce QuantifiersEngine::QEffort).
|
|
proofs. Filtering currently includes: LHS generalizes a term from an active conjecture, terms must be canonical, conjecture must be confirmed by a ground witness, and cannot be falsified by a ground witness. Refactoring of term database. QcfEngine now uses central data structure for term indexing. Add two options for quantifier instantiation : trigger selection mode --trigger-sel=mode, and --inst-no-entail which blocks all quantifier instantiations that are currently entailed (using an incomplete check).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
FMF for quantifiers over arrays.
|
|
|
|
|
|
|
|
|
|
for the report.
|
|
|
|
|
|
Segfaultfix
|
