mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-03 12:16:54 +00:00
Code Activity
21862 commits 46 branches 58 tags 186 MiB
Commit graph

21862 commits

This branch
This branch
All branches
Author SHA1 Message Date
dependabot[bot]
a7e3635931
Bump actions/upload-artifact from 6.0.0 to 7.0.0 
Bumps [actions/upload-artifact](https://github.com/actions/upload-artifact) from 6.0.0 to 7.0.0.
- [Release notes](https://github.com/actions/upload-artifact/releases)
- [Commits](https://github.com/actions/upload-artifact/compare/v6...v7)

---
updated-dependencies:
- dependency-name: actions/upload-artifact
  dependency-version: 7.0.0
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
 2026-03-02 23:40:26 +00:00
Nikolaj Bjorner
96285b0f91
Merge pull request #8824 from Z3Prover/copilot/fix-issues-except-rust 
Fix issues reported in discussion 8823 for all languages except Rust
 2026-03-02 10:35:31 -08:00
Nikolaj Bjorner
94809d413a
Merge pull request #8825 from Z3Prover/copilot/fix-reported-issues-8822 
Fix CSA-reported undefined behavior and uninitialized variables
 2026-03-02 10:03:16 -08:00
copilot-swe-agent[bot]
1461a53347 Fix TypeScript Array.fromFunc to use f.ptr instead of f.ast for Z3_func_decl type 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-02 16:22:08 +00:00
copilot-swe-agent[bot]
28fbe33114 Add missing API bindings: Python BvNand/BvNor/BvXnor, Go MkAsArray/MkRecFuncDecl/AddRecDef/Model.Translate, TS Array.fromFunc/Model.translate, OCaml Model.translate 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-02 00:21:57 +00:00
copilot-swe-agent[bot]
8e94cad8ab Fix static analysis findings: uninitialized vars, bitwise shift UB, garbage values 
- nla_core.cpp: Initialize j = null_lpvar in is_octagon_term
- bit2int.cpp: Initialize sign_p, sign_n, sz_p, sz_n
- act_cache.cpp: Initialize debug vars to nullptr
- enum2bv_rewriter.cpp: Use unsigned literal in 1u << idx
- bit_matrix.cpp: Use unsigned literal in 1u << (n-1)
- bit_util.cpp: Guard against bit_shift == 0 in shl/shr
- mpff.cpp: Cast exp to unsigned before shifting
- sorting_network.h: Guard against bits == 0
- dl_sparse_table.h: Use >= 64 instead of == 64

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-02 00:13:55 +00:00
copilot-swe-agent[bot]
122ee94935 Initial plan 2026-03-02 00:06:13 +00:00
copilot-swe-agent[bot]
8fad12fe18 Initial plan 2026-03-02 00:05:23 +00:00
Nikolaj Bjorner
dcb888d4c8
Merge pull request #8821 from Z3Prover/copilot/update-clang-analyzer-timeout 
Increase Clang Static Analyzer workflow timeout to 180 minutes
 2026-03-01 12:40:41 -08:00
copilot-swe-agent[bot]
51c84fb295 Increase Clang Static Analyzer workflow timeout from 90 to 180 minutes 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-01 20:18:45 +00:00
copilot-swe-agent[bot]
af201a8faf Initial plan 2026-03-01 20:14:45 +00:00
Nikolaj Bjorner
8a6d22d3f1
Merge pull request #8813 from Z3Prover/copilot/fix-issues-in-multiple-languages 
Fix API discrepancies for Go, Python bindings
 2026-03-01 12:09:23 -08:00
Nikolaj Bjorner
844731d99a
Merge pull request #8814 from Z3Prover/copilot/simplify-def-ref-smart-pointer 
Simplify def_ref smart pointer in model_based_opt.h
 2026-03-01 04:47:37 -08:00
copilot-swe-agent[bot]
a15c659e81 Add Python Optimize.translate() and missing Go tactic/simplifier functions 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-01 02:14:16 +00:00
copilot-swe-agent[bot]
23d194502a Simplify def_ref smart pointer: default ctor, init list, clearer bool, remove extra semicolon 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-01 02:10:19 +00:00
copilot-swe-agent[bot]
2b8615f4fc Add 8 missing BV overflow/underflow check functions to Go bindings 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-01 01:51:27 +00:00
copilot-swe-agent[bot]
137fd735f5 Initial plan 2026-03-01 01:49:00 +00:00
copilot-swe-agent[bot]
f80f279da9 Initial plan 2026-03-01 01:45:29 +00:00
Lev Nachmanson
38ab05e50a
Merge pull request #8805 from Z3Prover/qmbi_crash 
Fix assertion violation in q_mbi diagnostic output
 2026-02-28 11:28:51 -10:00
Lev Nachmanson
93ac330864 Fix assertion violation in q_mbi diagnostic output 
The IF_VERBOSE(0,...) block at line 498 in q_mbi.cpp used operator[]
on values2root map which asserts the key exists. When the model
evaluation of the inverted term produces a value not present in the
EUF values2root map, this crashes.

Use find() instead to handle the missing key gracefully, since this
is diagnostic output and the missing key is expected when the model
inversion produces inconsistent results.

Fixes assertion violation from #7027 (obj_hashtable.h line 168/174)
with forall/array/eq2ineq combination.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-02-28 11:15:28 -10:00
Lev Nachmanson
7968669cf2
Merge pull request #8803 from Z3Prover/mbo_leak 2026-02-27 19:02:56 -10:00
Lev Nachmanson
835da14afa
Update src/math/simplex/model_based_opt.h 
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
 2026-02-27 17:29:37 -10:00
Lev Nachmanson
9a1a407298
Merge pull request #8801 from Z3Prover/bvo 
Handle overflow predicates in new core bit-vector internalization
 2026-02-27 17:21:24 -10:00
Lev Nachmanson
fc6696c5e4 Fix memory leaks in model_based_opt def ref-counting 
Three bugs in the def ref-counting infrastructure:

1. dec_ref() incremented (++) instead of decrementing (--) the ref count,
   so objects were never freed.

2. def_ref lacked copy and move constructors, so the compiler-generated
   default copy just copied the raw pointer without inc_ref. This caused
   use-after-free when def_ref values were copied into vectors.

3. Compound def types (add_def, mul_def, div_def) lacked destructors to
   dec_ref their children. Added virtual destructor to base def class
   and child-releasing destructors to compound types.

Fixes the memory leak from #7027 (model_based_opt.cpp:81).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-02-27 17:15:20 -10:00
Copilot
f4abd88ff5
Add arity and bit-width SASSERTs to internalize_overflow (#8802) 
* Initial plan

* Add SASSERTs for arity and bit-width in internalize_overflow

Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
 2026-02-27 14:30:50 -10:00
Lev Nachmanson
2dac76d19a Handle overflow predicates in new core bit-vector internalization 
Add internalize_overflow() to handle OP_BUMUL_OVFL, OP_BSMUL_OVFL,
OP_BUADD_OVFL, OP_BSADD_OVFL, OP_BUSUB_OVFL, OP_BSSUB_OVFL,
OP_BSDIV_OVFL, and OP_BNEG_OVFL in the sat.euf=true solver path.

Previously these overflow predicates hit UNREACHABLE() in
internalize_circuit(). Now they are reduced to equivalent expressions
using existing BV operations and internalized via add_def().

Fixes the assertion violation from #7027 for bvuaddo and related
overflow predicates with tactic.default_tactic=smt sat.euf=true.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-02-27 13:07:39 -10:00
Lev Nachmanson
6ec40153cc fix #7677: treat FC_CONTINUE from check_nla as FEASIBLE in maximize 
When check_nla returns FC_CONTINUE it means NLA found constraint
violations and added lemmas. The current LP value is a valid lower
bound, so the status should be FEASIBLE, not UNBOUNDED.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-02-27 12:29:14 -10:00
Lev Nachmanson
ffe29b1433 Fix #7951: add cancellation checks to polynomial gcd_prs and HNF computation 
Add checkpoint() call in gcd_prs() main loop so polynomial GCD
computation respects rlimit/timeout. Add cancellation callback to
HNF calculation so it can be interrupted when the solver is cancelled.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-02-27 10:26:28 -10:00
Nikolaj Bjorner
d906a0cc2d fix bug reported by Maria Novoszel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-27 12:02:55 -08:00
Lev Nachmanson
5ff5b075b2
Merge pull request #8789 from Z3Prover/succ_int_mult 
Fix #7507: simplify (>= product_of_consecutive_ints 0) to true
 2026-02-27 09:45:26 -10:00
Lev Nachmanson
21c23e78db Fix #7507: simplify (>= product_of_consecutive_ints 0) to true 
The arith rewriter now recognizes that x * (x + 1) >= 0 for all
integers, since no integer lies strictly between -1 and 0.

Two changes:
1. is_non_negative: detect products where unpaired factors are
   consecutive integer expressions (differ by exactly 1), handling
   both +1 and -1 offsets and n-ary additions
2. is_separated: return true for (>= non_negative_mul 0), restricted
   to multiplication expressions to avoid disrupting other theories

Also adds regression tests for the new simplification.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-02-27 06:37:07 -10:00
Nikolaj Bjorner
fda8b4175f
Merge pull request #8793 from Z3Prover/copilot/fix-missing-api-functions 
Add missing array and FP API functions to Go, OCaml, and TypeScript bindings
 2026-02-27 03:14:18 -08:00
copilot-swe-agent[bot]
282db840de Add missing API functions to Go, OCaml, and TypeScript bindings 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-27 02:55:37 +00:00
copilot-swe-agent[bot]
3f6acc45ed Initial plan 2026-02-27 02:48:36 +00:00
Nikolaj Bjorner
ea873672c3
Merge pull request #8788 from Z3Prover/copilot/simplify-fpa-test-code 
refactor(test): extract run_fp_test helper in fpa.cpp
 2026-02-26 16:29:42 -08:00
copilot-swe-agent[bot]
cf0ffa2673 refactor: extract run_fp_test helper in fpa.cpp 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 23:54:17 +00:00
copilot-swe-agent[bot]
f2e00b3589 Initial plan 2026-02-26 23:52:54 +00:00
Nikolaj Bjorner
aeded4d721
Merge pull request #8787 from Z3Prover/dependabot/npm_and_yarn/src/api/js/multi-770cfcd984 
Bump minimatch in /src/api/js
 2026-02-26 15:52:39 -08:00
Nikolaj Bjorner
828e4a7ef7
Merge pull request #8779 from Z3Prover/copilot/convert-bv1-blast-to-simplifier 
Convert bv1-blast tactic to a dependent_expr_simplifier
 2026-02-26 15:52:18 -08:00
dependabot[bot]
e097a98019
Bump minimatch in /src/api/js 
Bumps  and [minimatch](https://github.com/isaacs/minimatch). These dependencies needed to be updated together.

Updates `minimatch` from 3.1.2 to 3.1.5
- [Changelog](https://github.com/isaacs/minimatch/blob/main/changelog.md)
- [Commits](https://github.com/isaacs/minimatch/compare/v3.1.2...v3.1.5)

Updates `minimatch` from 9.0.5 to 9.0.9
- [Changelog](https://github.com/isaacs/minimatch/blob/main/changelog.md)
- [Commits](https://github.com/isaacs/minimatch/compare/v3.1.2...v3.1.5)

---
updated-dependencies:
- dependency-name: minimatch
  dependency-version: 3.1.5
  dependency-type: indirect
- dependency-name: minimatch
  dependency-version: 9.0.9
  dependency-type: indirect
...

Signed-off-by: dependabot[bot] <support@github.com>
 2026-02-26 23:51:30 +00:00
Nikolaj Bjorner
c70f902b53
Merge pull request #8780 from Z3Prover/copilot/convert-blast-term-ite-to-simplifier 
Convert `blast-term-ite` tactic to a `dependent_expr_simplifier`
 2026-02-26 15:51:30 -08:00
Nikolaj Bjorner
fadf045df0
Merge pull request #8781 from Z3Prover/copilot/fix-ts-ocaml-issues 
Add register_on_clause to OCaml and TypeScript bindings
 2026-02-26 15:49:40 -08:00
copilot-swe-agent[bot]
ff7cc0f59e Remove old blast-term-ite tactic class, rename blast-term-ite2 to blast-term-ite 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 20:07:42 +00:00
copilot-swe-agent[bot]
668dd7a0a1 Rename bv1-blast2 to bv1-blast, remove old tactic source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 20:06:14 +00:00
Nikolaj Bjorner
a384e464e3
Merge pull request #8782 from Z3Prover/copilot/update-csa-workflow-discussion 
CSA workflow: embed raw report content directly into GitHub Discussion
 2026-02-26 09:27:56 -08:00
Nikolaj Bjorner
2105e95f30
Merge pull request #8785 from filipeom/filipe/expose-re_allchar 
Expose `mk_re_allchar` in OCaml API
 2026-02-26 09:26:51 -08:00
Filipe Marques
f0421879bb
Expose mk_re_allchar in OCaml API 2026-02-26 16:22:55 +00:00
Nikolaj Bjorner
070f760501
Merge pull request #8748 from Z3Prover/copilot/fix-floating-point-model-validation 
Fix fp.to_real bitvector encoding for denormal floating-point values
 2026-02-26 02:21:20 -08:00
copilot-swe-agent[bot]
234913bf56 Implement register_on_clause for OCaml and TypeScript bindings 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 04:04:27 +00:00
copilot-swe-agent[bot]
033ea50a5d Convert bv1-blast tactic to a simplifier 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 04:01:11 +00:00