Age | Commit message (Collapse) | Author |
|
|
|
RPM/Debian builds.
|
|
success, nonzero error
|
|
reporting this issue
|
|
|
|
|
|
|
|
derivative; disables loop detection when finite model finding is enabled.
|
|
|
|
|
|
turn off MBQI. Disable relevant triggers by default.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
model info. Also fix bug in model post-processor.
|
|
|
|
|
|
trans_closure, currently implemented a work around.
|
|
|
|
|
|
|
|
datatypes in type enumerator, fix infinite loop in type enumerator, fix fairness issue for splitting (moves constructor selection into model generation procedure), fixes bug 532, find conflict for constructor with conflicting label eagerly. Add representive flattening for quantifiers (currently disabled). Other minor cleanup.
|
|
sort inference and monotonicity. Minor cleanup.
|
|
|
|
especially for disequalities
|
|
|