4.8.6 release
Changes:
- 78ed71b update to pypirc
- bd26301 update to pypirc
- f8df777 na
- a1d3aca add release notes preparing for release
- 4b96238 use testpypi
- df2f041 undo atomic
- c68cfe8 #2565 use atomic
- 04ae000 fix #2567
- 9c74c05 address min-int overflow reported in #2565
- 77ef40a na
See More
- 4b51fe4 fix #2562
- 69abe16 backjump to level of clause to ensure that new atoms created by projection are assigned as assumptions fix #2557
- 0f20175 fix #2556, sign of of inequality is not restricted to -1, 0, 1, but can be -2, -3 etc
- 0c972b8 tidy
- da805f6 address perf bottleneck exposed by #2552
- fffc539 fix #2549
- 098725a fix #2553
- 67c4777 fix #2548 fix #2530
- 5d9ed5b Allow for
__truediv__and__rtruediv__even when not using Python3 - 1b83c67 spacer: fixes lim_num_generalizer
- 6384080 fix #2546, retrieve model in optsmt lex before iterating
- 0481adb fix #2547
- 0d3fed9 spacer: lemma generalizer for small numbers
- 78a1f53 fix #2544
- b1cdb3e add mbqi to smtfd. For Nuno, of course
- c22a17f smtfd
- d3da161 smtfd
- 5ba4d8d na
- d44081d fix clang compilation errors
- 3b1a73b add smt to project.py dependencies
- 85fb6f5 disable ackermannize on goal
- ff3cff0 deal with ite
- c476c4a smtfd solver that uses lazy iteration around fd to produce theory lemmas
- e881c4a Support repr_html for jupyter
- 228d68f enhance ackermannize for constant arguments
- 18ba14c Z3str3: fix empty-string contradictions (#2538)
- bc723fb fix #2539
- 8ec6219 na
- a92c82d na
- f645f8d fix #2537
- 29f0897 tweaking nlqsat
- 5fbfc0f minor code simplification
- 8f4e7f4 fix #2533
- 9fce5e1 fix build
- 87a96d7 fix mutexes hanging due to access to free'd memory
- cb75326 minor code simplification
- 68e4ed3 fix #2531
- 000e485 add array selects to basic ackerman reduction improves performance significantly for #2525 as it now uses the SAT solver core instead of SMT core
- 7823117 Restore expected behavior to stopwatch
- e816d16 fix #2527
- 4c0db00 fix push/pop bug for ite-elimination, thanks to Nao Hirokawa for reporting it
- de43e05 fix overflow bug exposed by #2476
- a8bfab3 add model.inline_def option to make #2517 happy
- 35fa24a initialize best model
- 20dc59e fix #2523
- 2e6908b fix #2509, fix issue with model inheritance exposed by #2483
- 271cd2a disable expensive model validation
- f048cb2 revert the revert
- 75a40d8 reorder fields, rename overload name clash
- 64f4c97 fix regressions during string fixes
- 0d9cd7b addressing misc. string bugs
- a337a51 fixes for #2513
- de69b01 Lev's fixes
- f90db2b add back compression to ensure local functions are inlined #2517
- c15764e remove verbose=0 instances #2507
- ffc696e exclude built-in functions from model
- eea0413 fix #2502
- e08abb3 fix #2504
- 2f60bcb Clean up NaN return values in Z3_get_numeral_double
- 423fb73 Fix for fp.rem. Pertains to #2381.
- f22d6e3 Fix floats in Z3_get_numeral_*string.
- 79cd1f0 Fixed Z3_get_numeral_double. Fixes #2501.
- 258b798 test-z3: Improve help output. Provide help when no args.
- f02170f Clean up whitespace.
- fcc7bd3 fix #2489
- 3074e2b fix #2487
- d64dc93 Add note about minimized unsat cores to C API docs.
- 9949f16 Fix release note typos.
- e2122c0 Fix whitespace issues in *.pyg.
- 0734c5f fix is-array-sort test again
- 892aa12 Fix for fp.rem. Fixes #2381.
- 0edd587 Fix typos in examples.
- ec5b148 Add python packaging build and deployment with Azure
- eec550e fix python build break
- 2b2f016 python for accessing lambda, switch to theory branching for QF_LRA
- 520ea65 move towards theory phase selection, implement getitem on lambda
- 0eafeb9 Fix confusing tabs mixed in with spaces in C examples.
- 0093157 Handle dynamic sort of Nth()'s return value in the Python API
- e89bb37 More see also content in C API docs.
- 375c0ff Implement get_proof() in bmc and spacer engines
- 876cfb4 optimization of phase
- 7596217 fix #2481
- 9fa9aa0 fix #2468, adding assignment phase heuristic
- 42e2145 fix #2479
- ce84e0f remove strategic solver header file
- fc41a61 expose strategic solver factory prototype at level of solver module
- 1ae0a98 fix #2466
- 52acbf1 bug in qe_lite
- e2d91ce distribute concat over bvxor and bvor, #2470
- 8579a00 distribute concat over bvxor and bvor, #2470
- e950453 force propagation for smt cubing
- bbfac99 fix #2469
- 0af249d 'na
- f90439f docs: Fix a number of identifier formatting issues.
- 077f518 Fix -Wreorder warning.
- ce7f9c3 Remove unused variable.
- d977c15 Merge pull request #2462 from waywardmonkeys/fix-typo
- 6be36f1 Fix typo.
- bc3b0f6 introduce fresh term when none is available in context or model to fix #2456
- 01920ab introduce fresh term when none is available in context or model to fix #2456
- 59f69bb introduce fresh term when none is available in context or model to fix #2456
- c7dc420 let me guess, ASAN doesn't like 0-byte memcpy
- 90415a1 fix build of test
- d7ac8db fix #2458
- 3147d23 fix #2460
- 4431a53 fix #2450 - track assumptions across lazy explanations and variable equalities
- db5af30 logging for #2450
- 1d488d0 nlsat
- 2d5714a fixing #2443 #2445 #2447 #2448
- 584eee2 fixing #2448 and #2445 and #2443
- c448033 fixing #2448 and #2445 and #2443
- 3d1c40c fixing #2448
- 95eb0a0 remove an unnecessary call m_mpq_lar_core_solver.m_r_solver.track_column_feasibility(j)
- 294dcf7 Merge pull request #2455 from levnach/fix
- e9e9500 fix the build
- db5ac5a fix a bug in lar_solver in queryaing if a column is int
- 9d6728a fix unsound rewrite
- 0a29002 return unknown if m_array_weak was used and result is satisfiable
- 3f032e8 remove include of thread
- bec38f2 remove debug code
- 7f073a0 fix #2452 fix #2451
- b7a27ca Merge pull request #2454 from RichardBradley/java_sudoku_example_fix
- 04e0b76 Fix sudoku Java example
- a2b18a3 fix #2449
- e1fd167 remove stale assertions due to lambda #2446
- 7463126 remove stale assertions due to lambda #2446
- 902c683 expose _get_ctx for scope semantics of newer versions of python #2441
- 2bd8d3b fixes for input4/5 #2416
- 06ee09a Update README.md
- 07472d2 Update README.md
- 7281395 unfinalize
- 42a1926 update readme
- 6b5961a update readme
- 00a4f6a throw
- 1d223b0 setting ctx to null after close
- 2eea770 Merge pull request #2438 from agurfinkel/issue_2430
- 53aded3 fix #2416 exposed bugs: unsat-core extraction in combination with chronological backracking, equivalence elimination in combination with PB constraints
- 92db639 Use refutation to compute ground sat answer
- 8a0d792 make sorting of soft constraints the same across implementations of std::sort
- e6df7b7 fix #2434
- ca25e48 temporarily disable elim_pure
- c75a577 fix #2433
- 859512d fix #2431
- e17b436 na
- 604e6b2 fix #2418, change types in sat_solver to avoid cast
- 809b0eb revert fix to #2417
- 3a90de1 fix #2419
- e65a5d0 fix #2420
- 019d78e fix #2422
- 1a70fce add back nvars
- 185b01d fix #2416
- c2264c7 debug mutex
- df04d7f Merge pull request #2428 from danielschemmel/warnings
- 77d5b38 Order initialization to avoid -Wreorder
- 5e5c231 Remove unused variables
- 364fbda expose reorder config
- aff4b30 fix #2417
- a9a26e5 review comments by Elffers
- e593b5b fix #2415
- 43a19ca avoid reorder regression. affects performance of SAT and also noticably for #2405
- 41ca956 expose import model converter over Python, document it, add partial order axioms for lex, disable linear order axioms, prepare ground for re-adding clauses from reconstruction stack
- 7ed5ca0 fix #2408
- d07f2d4 fix #2409
- 1fca76b relax restriction on infinitesimal for rdl, #2410
- 5820b16 mark assumption literals to be skolem to hide them from models #2406
- 4b6a737 insert fresh
- fb124d6 Merge pull request #2393 from Nils-Becker/master
- 4deb9d2 use array interpretations whenever possible for #2378. Also strengthen equality test for lambda
- 3ca32ef na
- 2d4e9a0 update managed APIs for lambda-based array models #2400
- 659be69 fix #2395
- 26c1c74 fix #2396
- 0bca2aa remove invocation of debugger
- 559af09 fix index cases
- 84990ff fixing #2378
- be72acc na
- 1538b31 na
- d861b91 augment axiomatization for substr to fix #2366
- 79e4b84 augment axiomatization for substr to fix #2366
- 1ba6d16 augment axiomatization for substr to fix #2366
- 308647e Merge branch 'master' of https://github.com/Z3Prover/z3
- 335072e extract logging into separate function
- cfb4d28 fix #2325
- c7fb1e4 fix spelling of target folder
- 9474833 fix #2391
- adb91ae compile 0 case regardless of numerical value
- 77df8eb try to copy artifacts
- 8d9a631 try to copy artifacts
- 1d859a9 updating comment
- 7a48524 count subterm references correctly
- b226f3a cleaning up includes
- 035101f Merge branch 'master' of https://github.com/Z3Prover/z3 into HEAD
- 23d01f5 fixing rewrite logging (https://bitbucket.org/viperproject/axiom-profiler/issues/13/version-486-of-z3-not-compatible-with)
- 09328d5 remove unknown option /RELEASE in python build
- ee94f8f update release script
- 5de35d4 fix #2390
- a13ac6a Merge pull request #2389 from agurfinkel/issue_2357
- 7cb956a Uses non-flattening rewriter in profos
- 88aa689 fix #2387, add ite-hoist rewriting, allow assumptions to be compound expressions
- cd93cdd na
- 6bbe8e2 add some static
- 6e63734 Merge pull request #2368 from waywardmonkeys/fix-typo
- 164039a Merge pull request #2383 from mcfi/patch-2
- dd253cd Merge pull request #2382 from mcfi/patch-1
- 962d0dd Pass /RELEASE to MSVC linker
- f8a9f6c Remove unreferenced formal parameter name
- 6d244ed internalize reflect
- b86432e na
- c744b19 resort to only supporting ground non-linear division for nra_tactic/nra_probe #2372 #2376
- 8e2ad4e #2379 and #2380
- 1517ca9 Another fix for fp.rem.
- 7782749 Added checkpoints to lia2card tactic.
- df40655 Cleaned up FP predicates in the Python API. Fixes #2323.
- e0dc05c Fixed final alignment step of fp.rem. Fixes #2369 and does not break #2289.
- 807095a fix #2375
- 1202554 Merge branch 'master' of https://github.com/z3prover/z3
- db87f2a separate rewriter used by smt context from asserted formulas to avoid term substitution, exposed by #2370
- c4e0f8c Python: Fix doc comment typo.
- 60c504f make a few helpers static
- e5dffea fix #2365
- 9009863 remove target from nightl'
- 218edbe ensure also negative lt are constrained #2360
- 85b0722 ensure also negative lt are constrained
- 1f0d162 fix segfault #2360
- 6f08c07 put back delete step in nightly
- 6e994f9 temporarily disable delete
- 8a129a3 try replace for nightly to address #2362
- 335543b adding comparison #2360
- db274eb relax condition for distributing extract over ite #2359
- b873427 pydoc regression
- 1e21ea4 fix cleanup bug exposed by reordering simplifcations
- e8080d2 revert normalizing ordering on equality as it breaks others and doesn't necessarily lead to simplification
- 2a1f8ac revert normalizing ordering on equality as it breaks others and doesn't necessarily lead to simplification
- 5dfc40b python regression
- b4290d4 python regression
- e0a4489 purge smt.timeout, use timeout instead to control solver timing #2354
- 63a952f setting ast to null on destructor to deal with #2350
- 333b32b disable adding redundant ite clauses as lemma. Add as non-redundant
- cbe52e2 remove tracing, fix doctext
- 1ae0769 update doctest
This list of changes was auto generated.