• bd8bed1759d823ed418e41050e6c95594e9d6ddf handle ac-op in legacy special relations procedure by adding warning
• 1b1ebaa3b03703cc76131e66c7cf9631685bf0ed minor simplification during internalization
• 36725383d342d30b012a252fd4f5a9285b8e4d1d minor simplification of terms during internalization.
• f06e07ad0a111e3de7cb1a203746a510ea631213 fix cone of influence computation for terms with nested variables [ #7027 ]
• 25dd29907b652bd22d2470bc0ca918c4d15a0b70 refine no-effect predicate to include value of ret
• 9cc2ce42f78fbb65982e097cac7f02113f95e366 #7027
• a8f3396b24740f157bdf12c60ed51fce24216005 #7033
• 965bee5801e95054d74d62a9749ba031e6179999 fix build
• 1de25ed09c0f3cf80d921a208946e0a15fa63c3d pending files
• b22daa98163b877bebe24f2d93e28d1e2f454a9f missing header
• 362d299a5ccfd6f4daad533d8209a1a28c9b0463 #7027
• ba8d8f0af746040f9c39f9da35c6acf30d3c0409 Disable hoist entirely, it is bad on QF_LIA and does not help on other observed cases
• 585d02766883de3f7087fc65d742ade814d45f8e remove assert #7032
• 331507c4cd9fbc06cdfede50c586217155bb6320 #7027
• 7eab26e3ef365cfab076dd13c23d9512dba16d08 try with missed bounds
• 5c1e7f711211e47e2710ac2c1caf35acf7dd1dec fix #7029
• ed5ab54ab60657f7e646346860c005889ae18fa5 CMake: Improve handling of git hash/describe (#7028)
• a15a7cee7bd7528e1e5b8e29f77083a03daa4ad8 touch
• faf14012ba18d21c1fcddbdc321ac127f019fa03 Regressions reported by Guido
• 99e2794a6db5aba5db6fd5eea55462e403eb886d update output
• 8a0dec1a4b2d05e04e12accac0540f1ca765d521 fix build
• b52fd8d9542dc51cd5c75496a9ee22b377fa04df add EUF plugin framework.
• 5784c2da795c90a1231e905b60eaaebccdbd95a4 remove an unnecessary if
• d540d881ef3d0d701e91ae8d7170ed2d74b529fa Add enter and exit methods to Solver class (#7025)
• 26440ed3d807cc5134ceefef28a3bd7d9ac367c4 deal with ubuntu/clang warnings
• e9abdbb7a4a55c38193a6b39af00c10742dfa457 fix #7011
• 9efe6f6afa5bef2975040b6e014ae9da149549e7 fix regression in fix for #7006
• faa2d8ac6c44e6306ee479ae08ddc848bf4c512f re-enable delayed literal propagation
• 2f01b5b567cff438b686c4b565130fc1e7f1abfe re-enable delayed literal propagation
• 4289cfac8d273c6bfd1b490e82fd68f5e9c1bce6 revert some fixes to euf
• 41a3196c890c9cff15b664679cd1cc0b951ad57f fix #7024
• d469c1054e4c06578a4bc12e869780dffc670a56 remove separate to_add_literal queue
• e972eb33b236272b93b8296a8f1df29043dd8c72 #6523 - contains_ptr bug regarding etable reinserts
• 1d4644f718fcc34db43bfab8040cd4f4246e0aa2 fix typos in script
• 79bbbf76d0c123481c8ca05cd3a98939270074d3 fix #7006
• 8179f8b5d7424c697d18afa5515f33e120f6bc32 fix #7017
• f36f21fa8c64c30c8a775ae6ca4950674bda33ae add comments for API versions of bit-vector overflow/underflow checks for #7011
• f90b10a0c8e7f292bbe6288452f6176d1d73e608 fix #7012
• 69f9640fdff33d196be69dc9e03e996b25e21389 fix #7018
• 3422f44cea4e73572d1e22d1c483a960ec788771 Fix syntax warning when using Python 3.12. (#7022)
• 8192b327e12277a6922260a6d5b5e483a6dcebb7 Bump mymindstorm/setup-emsdk from 12 to 13 (#7021)
• 9d1ceab1f28c032c71484b2a3772be514b645ad9 cmake: Use FindPython3. (#7019)
• b5e8f59eae631c35b55c1cee5c5d19cd8d6cde7d mbp: term: Fix reorder ctor warning. (#7016)
• 9d3fef3e2bdf6d1806aa9c2b171b1bb6f9d41d2f cmake: Require cmake 3.16 or later. (#7015)
• 2354998cd2c033b7c75d661ac60c1d9015180ab8 z3.h: Don't include stdio.h (#7014)
• a10c93e203f4892ce8176db7b2392a1121c1239b Bump docker/build-push-action from 5.0.0 to 5.1.0 (#7008)
• 16753e43f1ba11f9b32eeea3a76acc3015736696 Add accessors for RCF numeral internals (#7013)
• 9382b96a3250c1bfd1516211c5b3296e7a8b918f add API to access symbols associated with quantifiers
• d272acc3ac4169aaf0e1db89d674f1ae6e64faf9 fix crash when api_solver sets reset_tracked_assertions
• ac105b7d8c50c24d9cb27230591934212abd1064 remove unused code
• 4350bd77ac1ac759eaf51377d28d018df20b73ca check cancel flag to avoid unsound conflicts
• 32f8705ac32b9369955f02f465ccd3cd8e2abd7a #7001 - align is_numeral without to behavior if is_numeral with return numeral.
• 35bc522dae99fbafd1862d4c60336e8a0cc29517 #7003
• 924c2967049711ec73d318b5d7edc8873fbd1093 add logging
• 5bec982cc59fbbfeb87e5297e0bea2fdfadb4772 chores in theory_lra
• e40b8a2d13751fadd20de16e20803a1995ab6d82 household chores in legacy arithmetic solver
• 5ab1afe5c2e451f5d35f52867b1d58b69a4c85be expose enode pp convenciences
• 1710fe4927e0da90fc0ec921b41ad56e6e12d7e9 use iterator shortcut
• a9f9d3ddf4180ab8a9c6c353b64656d6eacbfd71 build fixes
• b9455c3692a8269d00a57b6c7a497b1f6e3b2068 #6999 deal with implicit assumptions, more robust pattern matching
• 6d6d6b8ed08be7363b774f8248572ef31e670963 build issue
• f94a475da386f2dd84a4711b03526648870644b6 Qel fixes (#6999) [ #6950, #6991, #6889 ]
• 1b6c7d65412fafa36a8c3a5fe0c8e195c1708c15 fix #6996
• 36382ccb5700428fb8ebdd3700d212cf8abe0be3 Fix memory and concurrency issues in OCaml API (#6992)
• 5b9fdcf46234ea241156c8450ba2c49674918444 fix #6997
• f1a39b888471ec6282717f26b17497b075ed068b add comment regarding usage model for flush_objects() to relate with pr #6992
• 3baaba5edd3a3a41c9c969e5ec9cf95006ac7429 Revert unsound NaN constraints in theory_fpa (#6993)
• c0ee4e96133ced638cc70240952f69ddb33fdd6d pip install importlib resources
• 1ce95d3859b4298d490487729ae416d32eab1fd5 pip install importlib resources
• 37b283fab96831cd54c05c4e7108438077a0a6aa use python3 in nightly
• 7ed27a1f416232ddf0b967d540cb5ea9bc4f62ce prepare release script
• ad2107f0792b36b801594c24b191673219d0a9d4 fix #6978
• 440601188135f02abd6353423297cd6c8a529288 fix #6984
• 3c2e97ddb6a37f36d873d62d257cd395fde3e700 fix #6988
• c2610cb37c214a1a58c4cd992bf0a2349d4fc6a2 #6523
• 8a4e8572944ad64cc4b7134173ca4183ae1d894a #6523
• 3de5af3cb0ad8b2481598a61065dbdd51525daba 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
• aa9c7912dc481de503c4dceff4b0b4acbba77444 fixed possible undefined variable assigment (#6985)
• 0556059bdfb697dd6fd3ba9e0855136f2b45b162 change to expr_ref to allow trying simplification
• bd4d580b17a15fc29256963e8d52d7d5449d6742 fix #6986
• e6385f8c858e6ff2b7e55d7f97f0d9767d8e3ba2 disable bound validation in debug mode
• 3d99ed9dd4e790a8bd90475fbde85e7275712fe6 Gomory cut / branch and bound improvements
• 9f0b3cdc2520bd089fe1ef4ef81a093960a20273 Add utility to expand sub-terms
• fb957601376865f9c8bad97df175dabb7d01a39b remove template
• 77dab53e9e480567b0fc5e655940fb0d6cca485d track number of Gomory cuts
• 2d1f4d5d93e348af5f7c94756c4d215bd51f49b0 remove verbose logging
• e86eae27e644370254e9ec2a9f6b9ff5434f682a #6523 and other heap-use-after-free error
• eed02b6d86cb149af89a860cdf92ce25fc880902 improved logging, use C++11 for loops instead of iterators
• 14312ef8a33991aa4ac460225fc5fe42e7afc2b1 remove some warnings with clang
• 08d3a82ce01bfd594d375354f318ee2a354deea1 simplify the jump on entering
• bdf1fcf5c126b64944ab8f4b28e70658700dd0df remove an assert
• ca6cb0af95ae15c063a33b3dd53a121586011501 add changes in lp with validate_bound and maximize_term
• ebd4d1a300c857bc48ce045ed23cab56580421cb WARNINGS_AS_ERRORS is ON/OFF, not TRUE/FALSE (#6979)
• 49a071988cec7aae927acd2084f7da79b89d70a5 remove temporary algebraic numbers from upper layers, move to owner module
• ea915e5b37ab43e4259b0e21c039d0a0dcac961e #6971
• 3af2b36cd73ad5377a9e0c76c013a057da4bc793 Add Z3_solver_interrupt to OCaml API (#6976)
• 91c2139b5dfa043af0a1d50a5591e662f1c1b6fb just use std::string
• fe6f38a160e916d1523c2db41baf9d6d50ae01c8 #6951, fix build
• c82b7dd2418fb8b1e0e4dd39cefde74a987bc169 Merge branch 'master' of https://github.com/z3prover/z3
• f97dd3402880963fe5b19ccbf144c3cce4e07cd7 tests
• 996b844cde66726ff3f4f2e95e1712df035031da Fixed parsing of | and \ (#6975)
• 938a89e197549d67f7e804fe1d395a03037b4a3e prepare for local version of Gomory cuts
• 160971df60d9c264a09c624fad041e66163ef651 fix #6969, again
• a957a5673dde8a316bba35e28bc323752a9ad3b6 remove experiment with theory lemmas
• 372696096944940bc35a12a27f186be0bfe76b60 fix #6969
• 589024aa1c13a7db71e496c7cec6c00fccfe9684 fix #6969
• 9d57bdd2ef2843ef6d1f8ff216c06854741fcc08 Assorted fixes for floats (#6968)
• bd8e5eee4b78587bf45ea9c12691914869fb4378 add simplification experiment (disabled) for tracking, some reshuffling of equation/fixed_equation structs
• e7c17e68b8281996b2d3d150de958dbceae21ec8 Fixed next_split call in pop (#6966)
• 52d16a11f9a56b6f650e61f0bd8d5455df08f0e1 deal with non-termination in new arithmetic solver
• f6c9ead10c0cf904925d7495f5c08dae66643b7a #6964
• 93427f1175783a541eff60d3b1cacb8cde052d76 regression test 2447
• 0b8d7b755d90557086b460af15caba406488b91d useful string rewrites
• 5622fd13622a24731ed8750a7ebda3d710a3e25b initialize delay bound
• 76f9e1d2b34524a583d156dc52d251119fceb73d fix build
• 702744f1397b46497e858fe2efbac89df7b1668f fix build
• 4434cee5df67251c3402ff881de48739e0f0756e merge
• 20c54048f79d9fb57650ca390c44be5a917e390a use cone of influence reduction before calling nlsat.
• e2db2b864bab5c3871e8da0ac2c36c2a61b1c11d add hook for in-processing simplification for NLA
• 6ba151599e4416604a3d6e5034cd49cf219b7926 Merge branch 'master' of https://github.com/z3prover/z3
• 55775bdc2054cc235208683e7db2bc4e0119c3ee incremnet log level for debug output on cancelation
• 236afeb8cb0257c916b3d2b0291bb9f3807665bb docs: More intra-doc linking, bit of formatting. (#6963)
• 7b490543ca72626e5b26dc164d91cabc2368e61c add missing simplification; handle nit #6952
• 0859be5649222241b385f53f1592d3d2000537f6 #6953
• d5fe4b0d78ef109582e9562adb9a67d33a8871ea Update script to use importlib_resources (#6949)
• f07c46a396b743d6cb7573a143a1e65685ed0617 Bump actions/setup-node from 3 to 4 (#6961)
• 8b040490697b79d93756aad69eea7291f2046983 Bump @babel/traverse from 7.19.4 to 7.23.2 in /src/api/js (#6954)
• aa703160cef2e4b78326961be16e2a6b7e34bdd9 Update README.md (#6960)
• 8fac89cdcc5291eb8234ba49fcc758499808951f enable more simplification in case inequality triggers a change.
• 4e21e126a8bef9e1035d67430593700d61a2683b update add_lemmas to use check-feasible
• c9d298e57fbf1ca06a1dfb41e307a40fc80fefe7 enable propagate-linear-equations and extend to monomials
• 53ce18ef347d8367634777c882f4d325bb489aee update backoff for bounded_nla
• 97058b0d5d8e9f3138479b5f77250f7477c29222 allow for propagations the trigger make-feasible check
• 8c00181815369de87b45bbe015b5606ec7b9b5f2 fix #6955
• 11ab583232c52d71a30311c3b7836beedb442835 fix #6956
• 37fe9cc764b7c98788813a071b82a241b46b9ad7 add Horner saturation to Grobner conflict detection
• 0a1cc4c054722b80f8cb682c5d20a947a0b22d0e fix exception safety in pdd-solver
• 3fa67777e5c7d4a4bf09e84a923a7ddca74696de fix exception safety in pdd-solver
• c9c5dbc347121791762cd3c1170cb691a3aa6831 #6523
• f678861aef8a49d53100d9d45fb28d04e49f81d5 fix #6947
• ba881d9c9bec76d690dbe3a8d6eef9ecbe78106f add facility to experiment with nla justified conflicts from Grobner equations
• 18fc6914d396241e928d43ba8a5c0d8531944b8b add facility to experiment with nla justified conflicts from Grobner equations
• bdac86501d6e27b8032925d6f9be02c5501bff0e add facility to check for missing propagations
• cafe3acff1d4aedf2b08a4700574fcb41b4e4355 delay detach
• 891ab8bac543d82a23cb0fd1f6d48b85f5c3acf1 #6523
• 6553382ec8f03663813da1e7a0de337dd76a2f50 remove extra assume-eqs
• b2efa592ce047d01a0023f548ab0fe299a1c9d55 #6523
• 41b1f47d77353e261d411fd382357626bf1c6c88 #6523
• 5942dc24bd90fcad262e94fcba88aa48bfbbebe1 #6523
• 5619ed05869f8e22cba4a49f3e00d9a4a63b5699 resurrect old bounds propagation
• a39d4adf5b67ab77966eac8146c6c3dbc406f7df build fixes
• 47f1c86f930b71efec93e5f787d51b82313c27d8 fix regression
• d44d78f9d1d51f4d9743c4e48fbf96644834d195 remove temporary configuration parameter used for testing
• 08af965b569328b15f2edcba35288a2efc97fb57 updates to monomial bounds
• ba6c23bbc5d2e080a75a159d82f8c5c934372c60 bug fix #6934 (#6940)
• fcb03aa56c193c5d53baa4d65105e25aa3404c4a minor code simplification
• 01188462d50cbd4f3f2a84b4930ab23d2ee1dd4a build
• 960a024d3d22388981e47c28d413d9a622cc069a fix build
• 6445d01557556c35626895ecaa80f490344ad6fb normalize newlines for if
• d04807e8c33900b1c86388319da6796afdc3772f merge
• 338d7b328352509cebb14ad0bf2176c74f8cdc2a remove unused variables
• f3e9712beb83b8f8194f93c17c34852c1c1237a9 formatting
• e8e636c3ec5a63fa0a3e7f3c4d94b943f9b9fccb fix #6936
• 7afa4d07523ad3dcd7e74d19c00f3169d6165e43 Merge pull request #6938 from Z3Prover/uprop
• 180ab727e73e591a0247aedd4997715f6deebd24 fix a bug in unit nl prop
• adbee0cd3fdfa9b9c7a3a96469e0bc9b8786b350 fix #6937
• 267e9e827db145d2986b789fad154ec44e80c1f0 #6935
• 4a870966ad1cf9ffc839c4b3d244cba521b7c0ee add code to enable unit propagation of bounds
• 1bdf66b918f3a4be5db5505a10388cfe70a138c5 move initialization to header file
• 75e29b2a6d2d007a69b6ae2fc747387554e45f01 Merge pull request #6905 from Z3Prover/unit_prop_on_monomials
• 1ba0f5aba944a28342a12ea194c663449fec3366 cosmetic changes
• 3aac528aef172ef97b41a3be7cf574801e5d9358 add a comment
• 54f7aac0bc51556906af6ef6c2e47e960c85055d column value is not necessarily at bounds
• 4c228fb02c056b95dcf1d099658dbe46b555b034 Merge branch 'master' into unit_prop_on_monomials
• a94a75459e7146d9f92ec960f59c681bfde0089b fixin nla_solver_test.cpp
• f847d039bc4f6c79874727f6da6cb2ecc070211b use the simple version of move_non_basic_column_to_bounds
• 19e921290e5c08c547b4ebe73752df262166b12c increase wasm stack size (#6931)
• 23de8056d70c38de5a0aee04ff1332a51bdb6040 Add RCF functions to OCaml API (#6932)
• bf3817ef7c1fd7db29135e258683c90ec2e88835 restore move_non_basic_to_bounds
• b61f4ac51f527416dc1a76ba1a76d1a55dfacec0 merge changes from master
• b0df74c1c1f4ab17b4aba4891bd7ab9b3457b748 #6930
• 45c0ed126e44bef4ff75d9179424f0c538a4f454 remove unnecessery call
• edd1761ff3c3bfbaff638526e3e78e97a20188e4 restore the scheme of m_columns_with_changed_bounds
• a88aa7ffa51769e607c5a6a9384a4f34f2320b74 debug new propagation scheme
• 00ba064cd3735ef8035edbbde4be7a0d71b4104c ensure bounds propagation on changed columns after nla propagation
• 4133a1cc5a94e1be0b7853b46fd7efa48358e8fb Fix UP registration in final callback (#6929)
• 7de06c4350fa7f387c1823e3c8f0ecdda45249e7 merging master to unit_prop_on_monomials
• a297a2b25c06ee541c8d414a060f93de0c770c16 fixes in lar_solver around nl unit propagation
• ab8fe199c59ac7721c0a8fe03c79af7aa77dd8a5 fix case for 0 multiplier in monomial_bounds
• 50654f1f4620bf58e132d44d3a22e48a17630922 add theory propagation to linear monomial propagation
• 702322a6e92ae794c8b8dd35de0b963e97795d81 change the order of lp and nlp propagation
• b64fdef41f4e1ff9b7c700d10541c7552286fa82 better tracking changinc rows and monomials
• f30a2c13be7384eda00ecc3e336bcf9a21f0fa8f propagate only one non-fixed monomial intrernally
• ddcd1ee992e999e061161e4541cf70d18d8d21b1 non-fixed term should have bound 0
• 65e59e3ec4ebd9c06469c15739a308d3c5f22d08 sketch of internal propagation
• 7207f0ff9c1cef27432b5345b60cc4ec85f57d70 sketch of internal propagation
• 29b5c47a8d416d2ab1ff2008626c845b58b25d01 track changed monics efficiently
• 9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca debug output with the variable that is fixed and its value
• 42767b9aab9e5ab87d27eb824389361e7dd64ea6 Merge branch 'master' into unit_prop_on_monomials
• 2297b0334b14a0141dd0a26d4d2942f83bb28ad9 re-introduce simple implementation of linear monomial propagation for evaluation
• 6559e5fb321c67530f5276751023575d86017953 port over std_vector and std-allocator functionality from monomial propagation branch
• aaa587398ea84ec5107ae9906bf5d665da262ffd 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
• 4b85a105bb48b1497242adf512c4f50e3f26e694 Merge branch 'master' into unit_prop_on_monomials
• 9c63ea31354d8e6b21013153f06c620acbd08a18 port over cosmetics from unit_prop_on_monomials branch
• 94eb10187339e52dd7e145f2ec6d4c9745c0d1a5 Merge branch 'master' into unit_prop_on_monomials
• 36566d619307927df6612696866f72e272d29de1 port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch
• ac6310d1a8fb131ef7765b20114868a7c289e104 Merge branch 'master' into unit_prop_on_monomials
• e4e1d6148c336a5d65337e27e04bfda85b528d9d port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch
• e8fcc876c9431999a36f5abc6b82d1aa47eb44da Merge branch 'master' into unit_prop_on_monomials
• ec2937e2debb85448c8c008e742a2dbac36a022f port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch
• 8d2b65b20bafa7cb016d44e9799047ecda4196fa add options to allow testing the effect of non-linear hammers
• 368fe80b3d31e946fbca1b4758994eb29aa26d1d fix the build
• 6ff4856e38fffa278c2a076ba18038199cddd12a throttle monomial unit prop and and nl params
• 896aba31f8b173a2108e7bf6fee778037acb4662 move monomial propagation from theory_lra to nla_solver
• d2c0f7dba797f3823f1c82f200e9d6acc98f01a5 fix test build
• 0a1ade6f9547040f7564623ec79fc1efbdf777a7 move m_nla_lemma_vector to be internal to nla_core
• 26a9b776c65076c647f9793fbe512ab43ff46d3e clean m_nla_lemma_vector in nla_solver
• 029d726eb8aabbf9bc0b7266f1e7aa27b05c1970 minor code simplification
• 87a839c794a78c0ac2962b5769b66e34b78fb653 fixup unit test for added argument to constructor of nla_solver
• 010a994a975c783f09eb4b7fe08044905c92113c Merge branch 'master' of https://github.com/z3prover/z3 into unit_prop_on_monomials
• db097bae0556c3cf40918ad15588d09d46f010b4 use format from unit_prop_on_monomials branch
• 3433366bef1076a45c52c248682e39d8dbc0556e Merge branch 'unit_prop_on_monomials' of https://github.com/z3prover/z3 into unit_prop_on_monomials
• 85eacf9bb1a13492804f0b7127d2a6f20078b5fe merge with master
• 61319ffd854fa144431d6fea4a0b433d4ac15bb2 cache is_shared information in the enode
• a3e2e68d93dcb4f2891e779fbe4419cc00db2b5e Update theory_lra.cpp
• acad9fa62c0cab9089ee385098e50545d544b2bb Update smt_context.cpp
• eea9c0bec61e7dd40603e2223ac0719bcc6997ba fix #6914
• 30d1800c3176b6bd6ca5a3e2c6109ad96784ba18 #6916
• 421fe946079ffb79ccae99bd85ffc6211c9570f7 rmove debug out
• 886d3f43511eb997dc16607daa24c75456f57532 indentation
• eac54ba084fb76d711b564a7c299317409945ac0 indentation
• 940775d12d1b214bdf010aae4f8476fbbefa9b9b indentation
• caa929f01f4ba66f5fcacd4e83c5fe7c7bfe363f do not use lemmase in monomial propagation
• 5d8779b05da3e47e032c5fcc0ef4ef072e30f3cc Merge branch 'master' into unit_prop_on_monomials
• eff3f5f65eecd6772b7a6827d31676785ab4443f port bug fixes from unit prop branch
• 576309a16fe8e6d30dd19bebaeaa1bc0b4856b6a Revert "reject rows with columns with big numbers for lp bound propagation"
• c0b55d14352fa76f3a2eabf346a8d20fb93b4e9e reject rows with columns with big numbers for lp bound propagation
• f423642e9b609eb4206519ef95cff4abff3910b1 try the lemma scheme
• e31cecf5dbe7b6d0542434451e8ed64497bd3075 transfer propagate monomial bounds to nla_solver
• 536930b4a160cf5e1f7260016629f0a17adc8459 make m_ibounds inside of lp_bound_propagator

This list of changes was auto generated.