z3-4.12.3

[NikolajBjorner]

4.12.3 release

Changes:

• 5e3f1d9 update release notes
• 4a9b38e clean up nla_grobner
• 84a7a79 fix invalid model issue on a QF_DT instance #7037
• f98b42a install importlib-resources for ubuntu doc
• de75692 install importlib-resources for ubuntu doc
• f7415bb install importlib-resources for ubuntu doc
• 17913f3 remove braces
• 18f1492 Clarify optimizer guarantees (Clarify optimizer guarantees #7030)
• 6910a4e Fix to_fp_signed (Fix fp.to_fp  #7034)
• ea3628e remove hoist functionality

See More

• bd8bed1 handle ac-op in legacy special relations procedure by adding warning
• 1b1ebaa minor simplification during internalization
• 3672538 minor simplification of terms during internalization.
• f06e07a fix cone of influence computation for terms with nested variables [ [consolidated] new core #7027 ]
• 25dd299 refine no-effect predicate to include value of ret
• 9cc2ce4 [consolidated] new core #7027
• a8f3396 Assertion violation at File: ../src/ast/ast.h Line: 952 #7033
• 965bee5 fix build
• 1de25ed pending files
• b22daa9 missing header
• 362d299 [consolidated] new core #7027
• ba8d8f0 Disable hoist entirely, it is bad on QF_LIA and does not help on other observed cases
• 585d027 remove assert ASSERTION VIOLATION, File: ../src/math/lp/lar_solver.cpp, Line: 1161 #7032
• 331507c [consolidated] new core #7027
• 7eab26e try with missed bounds
• 5c1e7f7 fix ASSERTION VIOLATION, File: ../src/qe/mbp/mbp_basic_tg.cpp, Line: 140 #7029
• ed5ab54 CMake: Improve handling of git hash/describe (CMake: Improve handling of git hash/describe #7028)
• a15a7ce touch
• faf1401 Regressions reported by Guido
• 99e2794 update output
• 8a0dec1 fix build
• b52fd8d add EUF plugin framework.
• 5784c2d remove an unnecessary if
• d540d88 Add enter and exit methods to Solver class (Add __enter__ and __exit__ methods to Solver class in Python API #7025)
• 26440ed deal with ubuntu/clang warnings
• e9abdbb fix signed-subtraction overflow: invalid unsat result #7011
• 9efe6f6 fix regression in fix for model completion for datatypes? #7006
• faa2d8a re-enable delayed literal propagation
• 2f01b5b re-enable delayed literal propagation
• 4289cfa revert some fixes to euf
• 41a3196 fix Invalid model on QF_NRA #7024
• d469c10 remove separate to_add_literal queue
• e972eb3 [consolidated] issues with new core #6523 - contains_ptr bug regarding etable reinserts
• 1d4644f fix typos in script
• 79bbbf7 fix model completion for datatypes? #7006
• 8179f8b fix Invalid model on QF_ANIRA #7017
• f36f21f add comments for API versions of bit-vector overflow/underflow checks for signed-subtraction overflow: invalid unsat result #7011
• f90b10a fix Feature request (Python): Overloading a few more operators to z3.BoolRef #7012
• 69f9640 fix Optimizers not producing optimal solutions when using assert_and_track #7018
• 3422f44 Fix syntax warning when using Python 3.12. (Fix syntax warning when using Python 3.12. #7022)
• 8192b32 Bump mymindstorm/setup-emsdk from 12 to 13 (Bump mymindstorm/setup-emsdk from 12 to 13 #7021)
• 9d1ceab cmake: Use FindPython3. (cmake: Use FindPython3. #7019)
• b5e8f59 mbp: term: Fix reorder ctor warning. (mbp: term: Fix reorder ctor warning. #7016)
• 9d3fef3 cmake: Require cmake 3.16 or later. (cmake: Require cmake 3.16 or later. #7015)
• 2354998 z3.h: Don't include stdio.h (z3.h: Don't include stdio.h #7014)
• a10c93e Bump docker/build-push-action from 5.0.0 to 5.1.0 (Bump docker/build-push-action from 5.0.0 to 5.1.0 #7008)
• 16753e4 Add accessors for RCF numeral internals (Add accessors for RCF numeral internals #7013)
• 9382b96 add API to access symbols associated with quantifiers
• d272acc fix crash when api_solver sets reset_tracked_assertions
• ac105b7 remove unused code
• 4350bd7 check cancel flag to avoid unsound conflicts
• 32f8705 Q: Enum sort numerals #7001 - align is_numeral without to behavior if is_numeral with return numeral.
• 35bc522 .NET application crashes with memory access exception #7003
• 924c296 add logging
• 5bec982 chores in theory_lra
• e40b8a2 household chores in legacy arithmetic solver
• 5ab1afe expose enode pp convenciences
• 1710fe4 use iterator shortcut
• a9f9d3d build fixes
• b9455c3 Qel fixes #6999 deal with implicit assumptions, more robust pattern matching
• 6d6d6b8 build issue
• f94a475 Qel fixes (Qel fixes #6999) [ ASSERTION VIOLATION, File: ../src/qe/mbp/mbp_basic_tg.cpp, Line: 139 #6950, Issue with tactic #6991, ASSERTION VIOLATION, File: ../src/qe/qe_mbp.cpp, Line: 572 #6889 ]
• 1b6c7d6 fix Assertion violation for quantified LIRA in new core #6996
• 36382cc Fix memory and concurrency issues in OCaml API (Fix memory and concurrency issues in OCaml API #6992)
• 5b9fdcf fix ASSERTION VIOLATION, File: ../src/math/lp/gomory.cpp, Line: 322 #6997
• f1a39b8 add comment regarding usage model for flush_objects() to relate with pr Fix memory and concurrency issues in OCaml API #6992
• 3baaba5 Revert unsound NaN constraints in theory_fpa (Revert unsound NaN constraints in theory_fpa #6993)
• c0ee4e9 pip install importlib resources
• 1ce95d3 pip install importlib resources
• 37b283f use python3 in nightly
• 7ed27a1 prepare release script
• ad2107f fix invalid model issue on an incremental QF_NIA instance #6978
• 4406011 fix ASSERTION VIOLATION, File: ../src/qe/qsat.cpp, Line: 580 #6984
• 3c2e97d fix Invalid model issue on QF_NRA #6988
• c2610cb [consolidated] issues with new core #6523
• 8a4e857 [consolidated] issues with new core #6523
• 3de5af3 fix bug in bound simplification in Gomory for mixed integer linear cuts, enable fixed variable redution after bugfix, add notes that rewriting bounds does not work
• aa9c791 fixed possible undefined variable assigment (fixed possible undefined variable assigment #6985)
• 0556059 change to expr_ref to allow trying simplification
• bd4d580 fix ASSERTION VIOLATION at File: ../src/math/lp/gomory.cpp, Line: 191 #6986
• e6385f8 disable bound validation in debug mode
• 3d99ed9 Gomory cut / branch and bound improvements
• 9f0b3cd Add utility to expand sub-terms
• fb95760 remove template
• 77dab53 track number of Gomory cuts
• 2d1f4d5 remove verbose logging
• e86eae2 [consolidated] issues with new core #6523 and other heap-use-after-free error
• eed02b6 improved logging, use C++11 for loops instead of iterators
• 14312ef remove some warnings with clang
• 08d3a82 simplify the jump on entering
• bdf1fcf remove an assert
• ca6cb0a add changes in lp with validate_bound and maximize_term
• ebd4d1a WARNINGS_AS_ERRORS is ON/OFF, not TRUE/FALSE (WARNINGS_AS_ERRORS is ON/OFF, not TRUE/FALSE #6979)
• 49a0719 remove temporary algebraic numbers from upper layers, move to owner module
• ea915e5 heap-use-after-free at math/polynomial/algebraic_numbers.h:371:40 #6971
• 3af2b36 Add Z3_solver_interrupt to OCaml API (Add Z3_solver_interrupt to OCaml API #6976)
• 91c2139 just use std::string
• fe6f38a Dead code in nla_basics_lemmas.cpp #6951, fix build
• c82b7dd Merge branch 'master' of https://github.com/z3prover/z3
• f97dd34 tests
• 996b844 Fixed parsing of | and \ (Fixed parsing of | and \  #6975)
• 938a89e prepare for local version of Gomory cuts
• 160971d fix :smtlib2_compliant setting makes the benchmark unknown #6969, again
• a957a56 remove experiment with theory lemmas
• 3726960 fix :smtlib2_compliant setting makes the benchmark unknown #6969
• 589024a fix :smtlib2_compliant setting makes the benchmark unknown #6969
• 9d57bdd Assorted fixes for floats (Assorted fixes for floats #6968)
• bd8e5ee add simplification experiment (disabled) for tracking, some reshuffling of equation/fixed_equation structs
• e7c17e6 Fixed next_split call in pop (Fixed next_split call in pop #6966)
• 52d16a1 deal with non-termination in new arithmetic solver
• f6c9ead python regression #6964
• 93427f1 regression test 2447
• 0b8d7b7 useful string rewrites
• 5622fd1 initialize delay bound
• 76f9e1d fix build
• 702744f fix build
• 4434cee merge
• 20c5404 use cone of influence reduction before calling nlsat.
• e2db2b8 add hook for in-processing simplification for NLA
• 6ba1515 Merge branch 'master' of https://github.com/z3prover/z3
• 55775bd incremnet log level for debug output on cancelation
• 236afeb docs: More intra-doc linking, bit of formatting. (docs: More intra-doc linking, bit of formatting. #6963)
• 7b49054 add missing simplification; handle nit Redundant checks in rpolynomial.cpp #6952
• 0859be5 Support constant rotating in bit-blast #6953
• d5fe4b0 Update script to use importlib_resources (Update script to use importlib_resources #6949)
• f07c46a Bump actions/setup-node from 3 to 4 (Bump actions/setup-node from 3 to 4 #6961)
• 8b04049 Bump @babel/traverse from 7.19.4 to 7.23.2 in /src/api/js (Bump @babel/traverse from 7.19.4 to 7.23.2 in /src/api/js #6954)
• aa70316 Update README.md (Update README.md #6960)
• 8fac89c enable more simplification in case inequality triggers a change.
• 4e21e12 update add_lemmas to use check-feasible
• c9d298e enable propagate-linear-equations and extend to monomials
• 53ce18e update backoff for bounded_nla
• 97058b0 allow for propagations the trigger make-feasible check
• 8c00181 fix Assertion Violation at ../src/qe/qsat.cpp:580 #6955
• 11ab583 fix Assertion Violation at ../src/smt/smt_internalizer.cpp:1112 #6956
• 37fe9cc add Horner saturation to Grobner conflict detection
• 0a1cc4c fix exception safety in pdd-solver
• 3fa6777 fix exception safety in pdd-solver
• c9c5dbc [consolidated] issues with new core #6523
• f678861 fix refutation unsoundness issue on an incremental QF_NRA instance #6947
• ba881d9 add facility to experiment with nla justified conflicts from Grobner equations
• 18fc691 add facility to experiment with nla justified conflicts from Grobner equations
• bdac865 add facility to check for missing propagations
• cafe3ac delay detach
• 891ab8b [consolidated] issues with new core #6523
• 6553382 remove extra assume-eqs
• b2efa59 [consolidated] issues with new core #6523
• 41b1f47 [consolidated] issues with new core #6523
• 5942dc2 [consolidated] issues with new core #6523
• 5619ed0 resurrect old bounds propagation
• a39d4ad build fixes
• 47f1c86 fix regression
• d44d78f remove temporary configuration parameter used for testing
• 08af965 updates to monomial bounds
• ba6c23b bug fix Issue with tactic #6934 (bug fix #6934 #6940)
• fcb03aa minor code simplification
• 0118846 build
• 960a024 fix build
• 6445d01 normalize newlines for if
• d04807e merge
• 338d7b3 remove unused variables
• f3e9712 formatting
• e8e636c fix heap-use-after-free at src/util/rlimit.cpp:90 #6936
• 7afa4d0 Merge pull request fix a bug in unit nl prop #6938 from Z3Prover/uprop
• 180ab72 fix a bug in unit nl prop
• adbee0c fix invalid model on an incremental QF_UFLIA instance #6937
• 267e9e8 Segfault on NIRA #6935
• 4a87096 add code to enable unit propagation of bounds
• 1bdf66b move initialization to header file
• 75e29b2 Merge pull request Unit propagation on monomials #6905 from Z3Prover/unit_prop_on_monomials
• 1ba0f5a cosmetic changes
• 3aac528 add a comment
• 54f7aac column value is not necessarily at bounds
• 4c228fb Merge branch 'master' into unit_prop_on_monomials
• a94a754 fixin nla_solver_test.cpp
• f847d03 use the simple version of move_non_basic_column_to_bounds
• 19e9212 increase wasm stack size (increase wasm stack size #6931)
• 23de805 Add RCF functions to OCaml API (Add RCF functions to OCaml API #6932)
• bf3817e restore move_non_basic_to_bounds
• b61f4ac merge changes from master
• b0df74c Performance issue with bitvectors combined with datatypes #6930
• 45c0ed1 remove unnecessery call
• edd1761 restore the scheme of m_columns_with_changed_bounds
• a88aa7f debug new propagation scheme
• 00ba064 ensure bounds propagation on changed columns after nla propagation
• 4133a1c Fix UP registration in final callback (Fix UP registration in final callback #6929)
• 7de06c4 merging master to unit_prop_on_monomials
• a297a2b fixes in lar_solver around nl unit propagation
• ab8fe19 fix case for 0 multiplier in monomial_bounds
• 50654f1 add theory propagation to linear monomial propagation
• 702322a change the order of lp and nlp propagation
• b64fdef better tracking changinc rows and monomials
• f30a2c1 propagate only one non-fixed monomial intrernally
• ddcd1ee non-fixed term should have bound 0
• 65e59e3 sketch of internal propagation
• 7207f0f sketch of internal propagation
• 29b5c47 track changed monics efficiently
• 9033b82 debug output with the variable that is fixed and its value
• 42767b9 Merge branch 'master' into unit_prop_on_monomials
• 2297b03 re-introduce simple implementation of linear monomial propagation for evaluation
• 6559e5f port over std_vector and std-allocator functionality from monomial propagation branch
• aaa5873 add propagation flag to monic and method for updating it to emonics. This replaces the bool-vector tracking for propagation and internalizes it to the emonics class
• 4b85a10 Merge branch 'master' into unit_prop_on_monomials
• 9c63ea3 port over cosmetics from unit_prop_on_monomials branch
• 94eb101 Merge branch 'master' into unit_prop_on_monomials
• 36566d6 port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch
• ac6310d Merge branch 'master' into unit_prop_on_monomials
• e4e1d61 port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch
• e8fcc87 Merge branch 'master' into unit_prop_on_monomials
• ec2937e port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch
• 8d2b65b add options to allow testing the effect of non-linear hammers
• 368fe80 fix the build
• 6ff4856 throttle monomial unit prop and and nl params
• 896aba3 move monomial propagation from theory_lra to nla_solver
• d2c0f7d fix test build
• 0a1ade6 move m_nla_lemma_vector to be internal to nla_core
• 26a9b77 clean m_nla_lemma_vector in nla_solver
• 029d726 minor code simplification
• 87a839c fixup unit test for added argument to constructor of nla_solver
• 010a994 Merge branch 'master' of https://github.com/z3prover/z3 into unit_prop_on_monomials
• db097ba use format from unit_prop_on_monomials branch
• 3433366 Merge branch 'unit_prop_on_monomials' of https://github.com/z3prover/z3 into unit_prop_on_monomials
• 85eacf9 merge with master
• 61319ff cache is_shared information in the enode
• a3e2e68 Update theory_lra.cpp
• acad9fa Update smt_context.cpp
• eea9c0b fix heap-use-after-free at src/ast/ast.h:507:36 #6914
• 30d1800 Inconsistent Results from consequences Interface Based on Constant Names #6916
• 421fe94 rmove debug out
• 886d3f4 indentation
• eac54ba indentation
• 940775d indentation
• caa929f do not use lemmase in monomial propagation
• 5d8779b Merge branch 'master' into unit_prop_on_monomials
• eff3f5f port bug fixes from unit prop branch
• 576309a Revert "reject rows with columns with big numbers for lp bound propagation"
• c0b55d1 reject rows with columns with big numbers for lp bound propagation
• f423642 try the lemma scheme
• e31cecf transfer propagate monomial bounds to nla_solver
• 536930b make m_ibounds inside of lp_bound_propagator

This list of changes was auto generated.

---

This discussion was created from the release z3-4.12.3.

[niyaznigmatullin]

It seems the arm64-glibc-2.35 (discussed in #6835) distribution is missing from the release; would it be possible to add that?

[NikolajBjorner]

see 4.12.4