z3-4.11.2
4.11.2 release
Changes:
- 8e6f17e inc version
- 1382cde release notes
- 85c8168 use for pattern instead of iterators
- 60967ef fix wrong condition for delayed bit-blasting
- 0bdb2f1 add verbose=1 log for mbp failure
- 7e1e64d fix #6313
- 9dca8d1 fix negative contains bug (#6312)
- e4ef171 fix variable tracking bug in explanations with literals
- eb1ea94 detect nested as-array in model values
- eb2b95e spacer: trying to make C++ happy
See More
- f2afb36 extend distinct check to ADT
- 61f7dc3 remove creation of trivial testers
- 46383a0 AG - unary datatypes, tester always is true.
- ac5b190 track instantiations from MBQI in proof logging for new solver
- d3e6ba9 remove union
- 3011b34 log E-matching based quantifier instantiations as hints
- 6077c41 #6116 bv2int bug fix
- f72cdda Change to 4 digit assembly version (#6297)
- 4abff18 fill in missing pieces of proof hint checker for Farkas and RUP
- d2b618d Spacer Global Guidance (#6026) [ #3 ]
- 1a79d92 revert last ditch array
- 36d76a5 fix #6304
- 45d8d73 #6303
- 0f475f4 Add RUP checking mode to proof checker.
- 8cb1182 add missing status case for cancelation
- cd0af99 fix #6302
- dd90689 build fixes
- 6f2a6da address unused variable warnings
- 4d29925 build fixes
- 8b8caf9 re-add smt-solver for proof_cmds
- 37fab88 respect dependencies, move proof_cmds to extra_cmds
- f65a244 move proof_cmds
- f5d2b9b fix typo in comment defining macros (#6306)
- a0ca5d7 Fixed nested user-propagator callbacks in .NET (#6307)
- e2f4fc2 overhaul of proof format for new solver
- 9922c76 add extra information for type error message
- dd91fab Merge branch 'master' of https://github.com/Z3Prover/z3
- 159026b regression fix to ackerman gc and memory smash, perf fix for handling bv2int axioms, perf fix for filtering ackerman
- 458f417 move drat functionality into euf
- 1ffbe23 add virtual destructor to fix build
- 1894c86 virtual
- ca0a829 add function pointer to class to see how MacOs build reacts
- 0d7b7a4 selectively re-add solver_params
- 5f2387b revert some changes that coincide with breaking macos build
- a628e4c updates to printer to get instantiations, take 1
- f0eee41 include depenency
- 6c165e8 #6299
- f6e151a assert
- d975886 fix #6300
- fb8532b succinct logging
- 74c61f4 move std::function to header of sat-drat - alignment?
- c626358 fix validator bug returning true for unprocessed case, bug reported in #6116
- ce1f398 fix unsoundness in quantifier propagation #6116 and add initial lemma logging
- 912b284 disable validate_hint too permissive
- 2f8b133 add redirect for warnings
- fbf9e30 ack
- fbfb28e update release notes
- 916d1db fix default parameter regression
- 7ab904b remove spurious file
- 0eea021 include global parameters and fixup for HTML meta-characters
- f6e4a45 Merge branch 'master' of https://github.com/z3prover/z3
- 64e0e78 #5953
- 09ab575 parens
- daa24ef add missing error check
- 9eb4237 fix #6292
- a383087 #6288
- 4092302 use interface for creating unary equalities
- 17fc438 don't have bv-ackerman influence simplification
- be0cd74 #6289
- 2181a0f #6289
- 56fb161 ADT-constructor generation crashed in .NET/Java when no (= default) fields are given (#6287)
- 6ba9ada Fix typos. (#6291)
- 706f7fb Fix some warnings about unused stuff. (#6290)
- d5d77df minor code simplifications
- 08bf7a6 fix name
- 665ef2c add missing new
- bb5d811 use equalities
- b26420e #6285
- ea8b118 Android CI: Configure with CMAKE_ANDROID_API (#6284)
- e83a70f add newlines for description
- 514eaf3 Merge branch 'master' of https://github.com/z3prover/z3
- 600b449 don't forget parameter documentation
- 540e36e roll version number
This list of changes was auto generated.