3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-14 16:25:11 +00:00

Commit graph

  • 82df1afeaf tentative solution: use existing nullability check (we might want to check in the future which guards of the ITE are actually true) c3 CEisenhofer 2026-04-14 18:07:03 +02:00
  • f09f6d5097 add internalization as fallback option Nikolaj Bjorner 2026-04-14 08:47:55 -07:00
  • 725b13680e na Nikolaj Bjorner 2026-04-14 08:35:48 -07:00
  • 0c4e4ad702 Regex factorization missed some justifications CEisenhofer 2026-04-14 17:19:07 +02:00
  • 2db99473a3 Removed irrelevant information from membership constraints CEisenhofer 2026-04-14 16:27:50 +02:00
  • 195f2caf25 Removed strange code that caused the solver to give up when finding a model instantly CEisenhofer 2026-04-14 16:06:03 +02:00
  • 3fdd903373 Bug if uninternalized literal becomes internalized and immediately false CEisenhofer 2026-04-14 15:48:13 +02:00
  • ed4387c70e Log to file CEisenhofer 2026-04-14 11:47:26 +02:00
  • acae332b13 add spp for easier pretty printing snode Nikolaj Bjorner 2026-04-14 00:39:01 -07:00
  • 53cc320efa deps Nikolaj Bjorner 2026-04-14 00:29:58 -07:00
  • 0258ec600f
    Merge c2d36054d1 into 1d19d4a0dc Guangyu (Gary) HU 2026-04-14 11:20:10 +08:00
  • c2d36054d1 Fix two bugs in Python examples Gary Hu 2026-04-14 11:09:19 +08:00
  • ce6faf2af9
    Merge 60b4dff428 into 1d19d4a0dc Ilana Shapiro 2026-04-13 18:54:51 -07:00
  • 60b4dff428 ablate to no backtracking on stale leases Ilana Shapiro 2026-04-13 15:49:54 -07:00
  • 88c472fc5e
    Merge d45b6365f3 into 1d19d4a0dc dependabot[bot] 2026-04-13 22:44:24 +00:00
  • d45b6365f3
    Bump actions/upload-artifact from 7.0.0 to 7.0.1 dependabot/github_actions/actions/upload-artifact-7.0.1 dependabot[bot] 2026-04-13 22:44:21 +00:00
  • 7cdd87b681
    Merge 729f4c7f01 into 1d19d4a0dc dependabot[bot] 2026-04-13 22:43:57 +00:00
  • 729f4c7f01
    Bump actions/cache from 5.0.4 to 5.0.5 dependabot/github_actions/actions/cache-5.0.5 dependabot[bot] 2026-04-13 22:43:54 +00:00
  • 7244f75c39
    Merge c4c8e828a9 into 1d19d4a0dc dependabot[bot] 2026-04-13 22:43:38 +00:00
  • c4c8e828a9
    Bump github/gh-aw-actions dependabot/github_actions/github/gh-aw-actions-ea222e359276c0702a5f5203547ff9d88d0ddd76 dependabot[bot] 2026-04-13 22:43:34 +00:00
  • 1b95686167
    Merge 0b0e617e08 into 1d19d4a0dc dependabot[bot] 2026-04-13 22:43:08 +00:00
  • 0b0e617e08
    Bump mymindstorm/setup-emsdk from 15 to 16 dependabot/github_actions/mymindstorm/setup-emsdk-16 dependabot[bot] 2026-04-13 22:43:05 +00:00
  • a3e3bfbaa2
    Merge afa02b6359 into 1d19d4a0dc dependabot[bot] 2026-04-13 22:43:03 +00:00
  • afa02b6359
    Bump actions/github-script from 8.0.0 to 9.0.0 dependabot/github_actions/actions/github-script-9.0.0 dependabot[bot] 2026-04-13 22:43:00 +00:00
  • e050781a11
    refactor(go): extract exprsToApps helper to eliminate duplication in QE projection functions simplify/go-api-qe-functions-becf1efa8d77b556 github-actions[bot] 2026-04-13 21:35:32 +00:00
  • dec2f2ec99 fix bug about backtracking condition being too strict: The epoch guard should not block backtrack(...) the same way it blocks try_split(...). A stale worker that proves UNSAT for n should still be able to close n, and that closure should then cancel the other workers on n and its subtree. Ilana Shapiro 2026-04-13 14:15:18 -07:00
  • ae1a456372 clean up code and add some comments Ilana Shapiro 2026-04-13 13:56:06 -07:00
  • 68d7917653 debug printing for widening Nikolaj Bjorner 2026-04-13 12:16:03 -07:00
  • 013f1db739 fix(parallel-smt): gate split/backtrack by lease epoch Ilana Shapiro 2026-04-13 11:59:00 -07:00
  • 035ea95faa add pp methods Nikolaj Bjorner 2026-04-13 11:41:49 -07:00
  • 150dff9459
    Merge c41753baad into 1d19d4a0dc Copilot 2026-04-13 18:11:01 +02:00
  • 4cd96eef93
    Merge 8e8799dbd3 into 1d19d4a0dc Don Syme 2026-04-13 18:11:00 +02:00
  • b5bd24056f
    Merge e6607df831 into 1d19d4a0dc Copilot 2026-04-13 18:11:00 +02:00
  • 2ca4690832
    Merge 9e96ee91dc into 1d19d4a0dc Copilot 2026-04-13 18:11:00 +02:00
  • c73b8e4d77
    Merge f0612ab7e0 into 1d19d4a0dc Copilot 2026-04-13 18:11:00 +02:00
  • 6ab0fcf286
    Merge d3f5fd6825 into 1d19d4a0dc Lev Nachmanson 2026-04-13 18:11:00 +02:00
  • eec5a6eda3
    Merge a37003fa2d into 1d19d4a0dc Lev Nachmanson 2026-04-13 18:11:00 +02:00
  • 9155ce85bb Removed unused function CEisenhofer 2026-04-13 15:05:41 +02:00
  • d620f20c63 Simplify code CEisenhofer 2026-04-13 14:06:06 +02:00
  • 276b9c38af log conflict Nikolaj Bjorner 2026-04-13 04:41:38 -07:00
  • fdba5445ec
    Merge a636fb3e83 into 1d19d4a0dc Copilot 2026-04-13 09:30:19 +02:00
  • 4f8d2c018f
    Merge 6b12bffd55 into 1d19d4a0dc Copilot 2026-04-13 08:53:26 +02:00
  • 18597c25cb
    Merge c49b403922 into 1d19d4a0dc Copilot 2026-04-12 18:27:48 -07:00
  • 1d19d4a0dc
    fix(qf-s-benchmark): add safeoutputs keepalive noop after build, reduce cap 500→300 (#9290) master Nightly Copilot 2026-04-12 18:26:55 -07:00
  • 4dfb6f7a7d display node state Nikolaj Bjorner 2026-04-12 15:45:03 -07:00
  • 1be70988b9 add logging for length / Parikh bug Nikolaj Bjorner 2026-04-12 15:34:22 -07:00
  • 01545ab9aa
    fix(qf-s-benchmark): add safeoutputs keepalive noop after build, reduce cap 500→300 copilot-swe-agent[bot] 2026-04-12 21:46:56 +00:00
  • 665d4f36ff
    Fixes for lar_term== operator (#9284) Arie 2026-04-12 17:31:18 -04:00
  • 717888572a
    simplify solve_eqs: move early return, replace ternary with if, fix indentation code-simplifier/solve-eqs-cleanup-2026-04-12-339acf93c4521357 github-actions[bot] 2026-04-12 21:01:41 +00:00
  • 68e528eaf7
    Go/OCaml API gaps: substitution, AST introspection, Spacer, Goal completion (#9277) Copilot 2026-04-12 14:00:03 -07:00
  • 6530a29eb1 Remove lp tests that use ineq::operator== Arie Gurfinkel 2026-04-12 16:54:43 -04:00
  • a86132095d Delete unused ineq::operator== Arie Gurfinkel 2026-04-12 13:43:53 -04:00
  • 95d28ad02c Fixed the model generation fix CEisenhofer 2026-04-12 19:34:11 +02:00
  • 1576824675 replace with e Nikolaj Bjorner 2026-04-12 10:17:46 -07:00
  • 7ddd8d5ab5
    Merge 1eb83ca9d4 into 1566d3cc41 Arie 2026-04-12 09:41:57 -07:00
  • 1566d3cc41 add flag to control non-linear substitutions: smt.solve_eqs.linear is by default false, setting it to true restricts solutions to substitutions to only use linear terms. This can have an effect on cross-multiplication of nested substitutions Nikolaj Bjorner 2026-04-12 09:41:46 -07:00
  • 276b00db5b Work around missing lar_term== Arie Gurfinkel 2026-04-12 09:39:20 -04:00
  • 81f242e45f Disable operator== for lar_term Arie Gurfinkel 2026-04-12 09:38:16 -04:00
  • fe100e7865 Fix broken term_comparer in m_normalized_terms_to_columns lookup Arie Gurfinkel 2026-04-07 11:54:43 -04:00
  • b341c61fbc first attempt with codex. Codex notes: What changed: Ilana Shapiro 2026-04-11 22:09:41 -07:00
  • 4c5aef4287
    fix: add substitute_funs to Expr module sig in z3.ml copilot-swe-agent[bot] 2026-04-11 19:21:31 +00:00
  • 67ed39caa7
    fix: address issues 1,2,4,5 and add Goal API to Go bindings copilot-swe-agent[bot] 2026-04-11 18:37:42 +00:00
  • 1544462f47 recompiled aw Nikolaj Bjorner 2026-04-11 11:17:51 -07:00
  • 853c62f58a
    Fix qf-s-benchmark: broken code fence, OOM build, and timeout budget (#9268) Copilot 2026-04-11 11:17:05 -07:00
  • 441661c959
    Merge branch 'master' into copilot/debug-zipt-string-solver-benchmark Nikolaj Bjorner 2026-04-11 11:16:51 -07:00
  • d29a1ebd38
    Fix Ostrich Benchmark workflow: allow NuGet and guarantee safe output (#9267) Copilot 2026-04-11 11:16:00 -07:00
  • f13a42bd22
    revert unaffected lock files to pre-PR state, keep only qf-s-benchmark compiled copilot-swe-agent[bot] 2026-04-11 18:15:55 +00:00
  • 6d92306fd3
    Merge branch 'master' into copilot/fix-ostrich-benchmark-workflow Nikolaj Bjorner 2026-04-11 11:15:46 -07:00
  • 4f308236c3
    recompile all workflow lock files with gh-aw v0.68.1 copilot-swe-agent[bot] 2026-04-11 17:22:06 +00:00
  • 2ce410d45e
    Fix Issue Backlog Processor: prevent context exhaustion by batching and requiring safe output (#9272) Copilot 2026-04-11 10:21:01 -07:00
  • 4a1f448a06
    Fix agentic workflow compilation errors (gh-aw v0.68 compat) (#9275) Copilot 2026-04-11 10:19:45 -07:00
  • b9e6a60898
    Fix agentic workflow compilation errors: remove glob/view tools, resolve merge conflict, fix serena tool and missing imports copilot-swe-agent[bot] 2026-04-11 17:16:24 +00:00
  • b34b7434e4
    Start: recompile agentic workflows, fix errors and security issues copilot-swe-agent[bot] 2026-04-11 17:14:22 +00:00
  • 2a142cd150 recompile aw Nikolaj Bjorner 2026-04-11 10:12:03 -07:00
  • 3c7e5c8197 add fold-unfold simplifier Nikolaj Bjorner 2026-04-10 18:03:54 -07:00
  • e0401a6544 fix truncation error Nikolaj Bjorner 2026-04-10 18:03:10 -07:00
  • 578db6643d
    Fix Issue Backlog Processor: limit batch size and require safe output copilot-swe-agent[bot] 2026-04-11 00:54:14 +00:00
  • 42ed906edf
    Initial plan copilot-swe-agent[bot] 2026-04-11 00:48:26 +00:00
  • 04bf2623fa
    fix(workflow): ZIPT Code Reviewer always call noop when no improvements found (#9269) Copilot 2026-04-10 17:47:54 -07:00
  • c9c4aa6b29
    fix ostrich-benchmark: add api.nuget.org to network allowlist and ensure safe output is always produced copilot-swe-agent[bot] 2026-04-10 21:39:11 +00:00
  • 6ca1bab43d
    fix qf-s-benchmark: Release mode build, fix broken code fence, reduce timeouts copilot-swe-agent[bot] 2026-04-10 21:38:10 +00:00
  • 6fdfec035b
    fix: instruct ZIPT Code Reviewer agent to call noop when no improvements found copilot-swe-agent[bot] 2026-04-10 21:36:39 +00:00
  • cc7a8d058a
    Initial plan copilot-swe-agent[bot] 2026-04-10 21:31:53 +00:00
  • b22d44867b
    Initial plan copilot-swe-agent[bot] 2026-04-10 21:31:34 +00:00
  • f64fc94675
    Initial plan copilot-swe-agent[bot] 2026-04-10 21:31:20 +00:00
  • 9c81571eb8
    Apply qf-s-benchmark fix: replace ZIPT/dotnet workflow with seq vs nseq only (#9266) Copilot 2026-04-10 14:30:44 -07:00
  • fafe159447
    Update qf-s-benchmark title prefix and note to QF_S Benchmark copilot-swe-agent[bot] 2026-04-10 21:21:25 +00:00
  • 11e02bda99
    Apply qf-s-benchmark fix from agentics/qf-s-benchmark.md: remove ZIPT/dotnet dependency copilot-swe-agent[bot] 2026-04-10 21:20:04 +00:00
  • 1eb83ca9d4 Introduce new monomials in Horner when shared factors have bounded linear combinations Arie Gurfinkel 2026-04-07 22:00:10 -04:00
  • 70e88e56fa Fix broken term_comparer in m_normalized_terms_to_columns lookup Arie Gurfinkel 2026-04-07 11:54:43 -04:00
  • 58ad1f0918
    Fix scaled_min test failure from #9235 mod-factor-propagation (#9260) Arie 2026-04-10 15:52:42 -04:00
  • e584895c98 Make model extraction a bit more stable CEisenhofer 2026-04-10 18:15:06 +02:00
  • 2b7204b07c Does model construction work properly now? CEisenhofer 2026-04-10 17:59:16 +02:00
  • 956fa85c1b Fix scaled_min test failure from #9235 mod-factor-propagation Arie Gurfinkel 2026-04-09 20:23:03 -04:00
  • 23ae00a57e update count to 2 copilot/fix-mcp-server-output-issues Nikolaj Bjorner 2026-04-09 16:39:27 -07:00
  • fbd51981c3
    mini_quip: port to Python 3 and fix several bugs (#9246) Guangyu (Gary) HU 2026-04-10 05:30:26 +08:00
  • 5ce8da8ade Fix scaled_min and max_reg test failures fix-scaled-min-max-reg-tests Lev Nachmanson 2026-04-09 12:12:31 -07:00
  • ceb363d35d
    SMTS tree algorithms (#9250) Ilana Shapiro 2026-04-09 09:46:47 -07:00
  • c7879ed5ad fix #9254 Nikolaj Bjorner 2026-04-09 09:19:40 -07:00
  • e6ef0d29c4 We need to check local consistency over and over again CEisenhofer 2026-04-09 15:56:00 +02:00