Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
timing)
|
|
particular kind can be set by setting interpreted = true when calling addFunctionKind.
|
|
|
|
|
|
references)
|
|
|
|
quantifier body uses them in term context
|
|
|
|
|
|
|
|
|
|
|
|
and src
|
|
x = c iff x = d ---> false
This fixes Andy's problem if unconstrained simplification is turned on.
|
|
boolean terms, improvement for pre skolemization
|
|
* For example, (_ bv5 1) is now an error instead of being silently truncated.
* Probably inappropriate for 1.0.x because it changes exception specifications.
|
|
|
|
miniscoping option --ag-miniscope-quant, minor cleanup
|
|
Conflicts:
src/smt/smt_engine.cpp
|
|
|
|
|
|
(Cherry-picked from commit c71ec27 in master.)
|
|
|
|
|
|
|
|
|
|
datatype enumerations + minor update to array rewriter to improve output for this option, minor refactoring of representative selection for quantifier instantiation, initial draft of disequality propagation option --uf-ss-deq-prop, other refactoring of uf strong solver, fixed bug 496, improvement for fmf enumeration of finite built-in sorts
|
|
|
|
|
|
|
|
|
|
|
|
decision/ code refactoring
|
|
|
|
other minor: cleanup some remaning fragments of GiveUpException(),
hopefully all is gone now.
|