Overview
Request 999657 accepted
- update to 4.11.0:
* remove Z3_bool, Z3_TRUE, Z3_FALSE from the API. Use bool, true, false instead.
* z3++.h no longer includes as it did not use it.
* add solver.axioms2files
- prints negated theory axioms to files. Each file should be unsat
* add solver.lemmas2console
- prints lemmas to the console.
* remove option smt.arith.dump_lemmas. It is replaced by solver.axioms2files
* add option smt.bv.reduce_size.
- it allows to apply incremental pre-processing of bit-vectors by identifying ranges that are known to be constant.
This rewrite is beneficial, for instance, when bit-vectors are constrained to have many high-level bits set to 0.
* add feature to model-based projection for arithmetic to handle integer division.
* add fromString method to JavaScript solver object.
Request History
elimat created request
- update to 4.11.0:
* remove Z3_bool, Z3_TRUE, Z3_FALSE from the API. Use bool, true, false instead.
* z3++.h no longer includes as it did not use it.
* add solver.axioms2files
- prints negated theory axioms to files. Each file should be unsat
* add solver.lemmas2console
- prints lemmas to the console.
* remove option smt.arith.dump_lemmas. It is replaced by solver.axioms2files
* add option smt.bv.reduce_size.
- it allows to apply incremental pre-processing of bit-vectors by identifying ranges that are known to be constant.
This rewrite is beneficial, for instance, when bit-vectors are constrained to have many high-level bits set to 0.
* add feature to model-based projection for arithmetic to handle integer division.
* add fromString method to JavaScript solver object.
jirislaby accepted request
lgtm, thanks
