- Update to version 4.4.1+git.20160717:
  * fix bugs exposed in #677. to_int(x) has the semantics that to_int(x) <= x, and to_int(x) is the largest integer satisfying this inequality. The encoding in purify_arith had it the other way x <= to_int(x) contrary to how to_int(x) is handled elsewhere. Another bug in theory_arith for mixed-integer linear case was also exposed. Fractional bounds on expressions of the form to_int(x), and more generally on integer rows were not rounded prior to internalization
  * garbage collect all api::object references when calling del_context. Request issue #679
  * add proper garbage collection to ast_manager. Issue #679
  * remove unfinished ite-macro finder, tune ast GC to ensure nodes are roots only once
  * fix rounding mode for pseudo-boolean constraint creation, Issue #683
  * add object z3 objects to target context during translation, to fix build regression failure on z3test.py
  * add tptp5 example to cmake, adding output SZS directives for Geoff
  * fix ubuntu build failure
  * mark also ast in parameters as GC roots. Issue #676
- Use cmake macros
- Some spec file polishing with spec-cleaner

• Files Changed
• Browse Source