| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
Conflicts:
src/smt/boolean_terms.cpp
|
|
due to namesapce resolution std namespace was used instead, which hashes the string pointers leading to mayhem
|
|
|
|
export CXXFLAGS='-std=gnu++0x' before configure
fails all regressions in the parser
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
