3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-10 14:35:33 +00:00

Commit graph

  • 51f3996464 Create dummy sat-node to avoid problems in case the preprocessor solves the problem entirely CEisenhofer 2026-03-19 16:02:51 +01:00
  • 9f4e823c8b ... and another one... CEisenhofer 2026-03-19 15:44:15 +01:00
  • 4271bdad55 Another minterm bug CEisenhofer 2026-03-19 15:12:22 +01:00
  • 149a087f65 Strengthened diseq axiom CEisenhofer 2026-03-19 11:14:07 +01:00
  • c07f897d8c theory_nseq: add enqueue/dequeue_axiom + std::variant prop_item + relevant_eh copilot-swe-agent[bot] 2026-03-19 04:47:34 +00:00
  • 398d2b3830 fix build: remove stale snode_label_html declaration from seq_nielsen.h copilot-swe-agent[bot] 2026-03-19 04:23:24 +00:00
  • f837651434
    seq_nielsen: replace mk_fresh_var() with mk_fresh_var(sort* s) (#9037) Copilot 2026-03-18 20:41:41 -07:00
  • 745b0291c1 Print full child output for all tests in parallel mode Lev Nachmanson 2026-03-18 15:17:56 -10:00
  • d6fc41cdaf Make parallel execution the default for test-z3 Lev Nachmanson 2026-03-18 15:07:33 -10:00
  • 4f32152f75 Add parallel test execution to test-z3 (/j flag) Lev Nachmanson 2026-03-18 14:57:16 -10:00
  • a271cc09d5 fix #9036: expand bounded integer quantifiers in qe-light Lev Nachmanson 2026-03-18 13:24:10 -10:00
  • 3aa6a5f7d2 dispatch assign_eh cases via m_axioms: add prefix/suffix/contains true axioms copilot-swe-agent[bot] 2026-03-18 22:36:56 +00:00
  • 4b40969da6 added diseq Nikolaj Bjorner 2026-03-18 13:32:18 -07:00
  • b42de8c676 remove mk_var(symbol const&) from sgraph; update all callers to pass sort explicitly copilot-swe-agent[bot] 2026-03-18 20:00:31 +00:00
  • a2352529f8 add diseq axiom Nikolaj Bjorner 2026-03-18 12:58:17 -07:00
  • 777bda01a5 Subsolver was not reset properly CEisenhofer 2026-03-18 20:22:08 +01:00
  • 426b7963bf replace mk_fresh_var() with mk_fresh_var(sort* s) in seq_nielsen; fix snode_label_html linkage copilot-swe-agent[bot] 2026-03-18 18:08:55 +00:00
  • a37003fa2d fix #8185: add FPA rewriter simplifications for fma with zero multiplicand and classification of int-to-float conversions iss8185 Lev Nachmanson 2026-03-18 07:30:55 -10:00
  • c43df60182 fix build of unit tests Nikolaj Bjorner 2026-03-18 10:29:41 -07:00
  • 23b7e109bd partial updates to test copilot/fix-build-errors-z3-test Nikolaj Bjorner 2026-03-18 10:01:47 -07:00
  • 8ac8eb4ae7 create sub-class for tracked eq and mem relations to separate from seq_nielsen Nikolaj Bjorner 2026-03-18 09:46:49 -07:00
  • e7431400b4 Regex bug fixes (still not there) CEisenhofer 2026-03-18 18:01:44 +01:00
  • 983379f5e2 Missing semicolon CEisenhofer 2026-03-18 16:16:59 +01:00
  • 0a32337f0a Removed some brackets CEisenhofer 2026-03-18 16:15:37 +01:00
  • d8a6ea1321 Fixed crasb if regex is reported SAT by pre-check CEisenhofer 2026-03-18 16:08:02 +01:00
  • 579ac6bfc4 Updated script CEisenhofer 2026-03-18 15:45:56 +01:00
  • 43950569eb More fixes CEisenhofer 2026-03-18 15:41:27 +01:00
  • b288c2e7dc Some more bug fixes CEisenhofer 2026-03-18 14:54:12 +01:00
  • ab53889c10 Fixed couple of regex problems [there are still others] CEisenhofer 2026-03-18 14:28:53 +01:00
  • b5bf4be87e fix: move m_fixed insertion after check_long_strings guard Lev Nachmanson 2026-03-17 15:40:45 -10:00
  • 960ab8e67a perf: move check_fixed_length(false,true) before check_contains in final_check_eh copilot-swe-agent[bot] 2026-03-18 01:05:56 +00:00
  • 8909919d6d
    Potential fix for pull request finding Lev Nachmanson 2026-03-17 15:56:00 -10:00
  • ba579549eb fix: move m_fixed insertion after check_long_strings guard Lev Nachmanson 2026-03-17 15:40:45 -10:00
  • ba15870935 perf: move check_fixed_length(false,true) before check_contains in final_check_eh copilot-swe-agent[bot] 2026-03-18 01:05:56 +00:00
  • 09c13a75e3 fix #8023: don't skip axiom clauses with non-base-level satisfying literals Lev Nachmanson 2026-03-17 07:22:23 -10:00
  • 0bf8fdebe7 Initial plan copilot-swe-agent[bot] 2026-03-18 00:12:09 +00:00
  • c41753baad Initial plan copilot/fix-fpa-soundness-issue copilot-swe-agent[bot] 2026-03-18 00:09:12 +00:00
  • d3f5fd6825 Fix Java UnsatisfiedLinkError on macOS (#7640) fix-java-macos-unsatisfied-link-error-7640 Lev Nachmanson 2026-03-17 13:59:37 -10:00
  • b1bae695e6 comment Nikolaj Bjorner 2026-03-17 16:32:01 -07:00
  • 2847dd8bb3 small simplification Nikolaj Bjorner 2026-03-17 16:30:53 -07:00
  • 3719b449e8 re-organize dependencies Nikolaj Bjorner 2026-03-17 16:18:27 -07:00
  • 3745bdd43b fix: reduce verbose lock contention in theory_diff_logic (issue #8019) copilot-swe-agent[bot] 2026-03-17 19:10:42 +00:00
  • c00d47b55b fix #8185: invalid model validation with division by zero Lev Nachmanson 2026-03-17 12:49:39 -10:00
  • 0461e010bb assign every new issue to copilot by default Lev Nachmanson 2026-03-17 12:09:01 -10:00
  • a61bcf0532 fix: reduce verbose lock contention in theory_diff_logic (issue #8019) copilot-swe-agent[bot] 2026-03-17 19:10:42 +00:00
  • b27409e8b0 fix #8023: don't skip axiom clauses with non-base-level satisfying literals Lev Nachmanson 2026-03-17 07:22:23 -10:00
  • c77c4bc7f9 Initial plan copilot-swe-agent[bot] 2026-03-17 18:35:48 +00:00
  • 027a4b8be3 Initial plan copilot/issn000-fix-issue copilot-swe-agent[bot] 2026-03-17 16:49:37 +00:00
  • 7d78a19f1c Convert dep_source to std::variant<dep_eq, dep_mem> copilot-swe-agent[bot] 2026-03-17 03:47:48 +00:00
  • af3729ef31 Initial plan copilot-swe-agent[bot] 2026-03-17 03:24:13 +00:00
  • a252121945
    Bump actions/download-artifact from 8.0.0 to 8.0.1 (#9016) dependabot[bot] 2026-03-16 16:11:55 -07:00
  • 103bf6dc35
    Bump github/gh-aw from 0.53.4 to 0.59.0 (#9015) dependabot[bot] 2026-03-16 16:07:29 -07:00
  • cc1a801992
    Bump actions/download-artifact from 8.0.0 to 8.0.1 dependabot[bot] 2026-03-16 22:54:14 +00:00
  • 9d033f304a
    Bump actions/setup-python from 5 to 6 (#9017) dependabot[bot] 2026-03-16 15:52:45 -07:00
  • 0564dfe32b
    Bump actions/checkout from 5.0.1 to 6.0.2 (#9018) dependabot[bot] 2026-03-16 15:52:35 -07:00
  • ef22ae8871
    Replace dep_tracker uint_set with scoped_dependency_manager<dep_source> in seq_nielsen (#9014) Copilot 2026-03-16 15:52:18 -07:00
  • cb1a26c668
    Bump actions/checkout from 5.0.1 to 6.0.2 dependabot[bot] 2026-03-16 22:15:28 +00:00
  • 82291afa8b
    Bump actions/setup-python from 5 to 6 dependabot[bot] 2026-03-16 22:14:45 +00:00
  • 0b535bb000
    Bump github/gh-aw from 0.53.4 to 0.59.0 dependabot[bot] 2026-03-16 22:14:07 +00:00
  • 5125858a00 fix test build: update dep_tracker usages in test files and seq_state.h copilot-swe-agent[bot] 2026-03-16 21:56:40 +00:00
  • 39bf6af870 Missing file edits CEisenhofer 2026-03-16 21:10:40 +01:00
  • e439504ec8 Delete cached substitutions completely (for now) to avoid dangling pointers after backtracking CEisenhofer 2026-03-16 21:04:47 +01:00
  • f4adcde585 add regression test for #9012: box mode mod optimization Lev Nachmanson 2026-03-16 09:47:09 -10:00
  • cdcdf263f1 replace dep_tracker uint_set with scoped_dependency_manager<dep_source> copilot-swe-agent[bot] 2026-03-16 19:05:35 +00:00
  • 84d371f2e9 Bugfix in regex overapproximation CEisenhofer 2026-03-16 19:54:12 +01:00
  • 1c232b96fd Initial plan copilot-swe-agent[bot] 2026-03-16 18:40:15 +00:00
  • f03cac6e51 fix #9012: incorrect optimization of mod in box mode Lev Nachmanson 2026-03-16 07:28:34 -10:00
  • 16f693b09a Regex intersection bug fixe CEisenhofer 2026-03-16 16:30:20 +01:00
  • 256f1bdf1a remove non-compiling timeout code Nikolaj Bjorner 2026-03-15 21:39:14 -07:00
  • 32eedde897 disable rewrite that makes nseq solving harder Nikolaj Bjorner 2026-03-15 21:36:22 -07:00
  • db8a2f4f9e update print and cancelation Nikolaj Bjorner 2026-03-15 20:43:49 -07:00
  • 7dea14f732 move statistics Nikolaj Bjorner 2026-03-15 20:09:19 -07:00
  • d137f25b65 na Nikolaj Bjorner 2026-03-15 19:58:21 -07:00
  • d15aed0d04 code organization in theory_nseq Nikolaj Bjorner 2026-03-15 19:39:53 -07:00
  • fe6efef808
    Add monthly Academic Citation & Research Trend Tracker workflow (#9007) Copilot 2026-03-15 15:39:37 -07:00
  • 99099255b6 Fix inconsistent optimization with scaled objectives (#8998) Lev Nachmanson 2026-03-15 07:02:13 -10:00
  • 5df80705aa Fix inconsistent optimization with scaled objectives (#8998) Lev Nachmanson 2026-03-15 07:02:13 -10:00
  • 47fd5ef9c6 nseq: refactor to propagate_length_constraints called from propagate() copilot-swe-agent[bot] 2026-03-15 20:41:48 +00:00
  • dfd75ec2de nseq: use theory propagation in propagate_regex_length_bounds copilot-swe-agent[bot] 2026-03-15 20:19:38 +00:00
  • a8d91cbec0 Replace get_power_exponent() with snode::get_power_exp() across seq_nielsen copilot/update-euf-snode-support copilot-swe-agent[bot] 2026-03-15 20:01:36 +00:00
  • fbeb4b22eb
    Add missing Go Goal/FuncEntry/Model APIs and TypeScript Seq higher-order operations (#9006) Copilot 2026-03-15 12:57:44 -07:00
  • daac7d3417 Add academic-citation-tracker workflow and compiled lock file copilot-swe-agent[bot] 2026-03-15 19:43:55 +00:00
  • f01287db46 Initial plan copilot-swe-agent[bot] 2026-03-15 19:39:10 +00:00
  • 9f061b4707 refactor: use arg() accessor in get_power_base/get_power_exp copilot-swe-agent[bot] 2026-03-15 19:34:47 +00:00
  • 8fdb491c1b refactor: use arg(0)/arg(1) instead of seq_util in power accessors copilot-swe-agent[bot] 2026-03-15 19:33:01 +00:00
  • a4c9a5b2b0 add review comments Nikolaj Bjorner 2026-03-15 12:23:17 -07:00
  • 5d02828c9d Initial plan copilot-swe-agent[bot] 2026-03-15 19:14:25 +00:00
  • 6893674392
    fix: correct misleading API comments in fp.go and JavaExample.java (#9003) Copilot 2026-03-15 12:08:59 -07:00
  • 77fafec3ff Fix nseq regex gap: increase BFS limit, eager length propagation, relax precheck SAT condition copilot-swe-agent[bot] 2026-03-15 19:03:47 +00:00
  • 8105cd21c3 Fix inconsistent optimization with scaled objectives (#8998) Lev Nachmanson 2026-03-15 07:02:13 -10:00
  • ee1ebed1cf fix: correct misleading API comments in fp.go and JavaExample.java copilot-swe-agent[bot] 2026-03-15 18:17:57 +00:00
  • bb8eb7f779 fix: add missing API bindings from discussion #8992 for Go and TypeScript copilot-swe-agent[bot] 2026-03-15 18:17:24 +00:00
  • b549c50af6 Initial plan copilot-swe-agent[bot] 2026-03-15 18:14:46 +00:00
  • d5a74647c3 Initial plan copilot-swe-agent[bot] 2026-03-15 18:12:30 +00:00
  • 5fcb673c58 Initial plan copilot-swe-agent[bot] 2026-03-15 18:09:09 +00:00
  • bebad7da50
    Add numeral extraction helpers to Java API (#8978) Angelica Moreira 2026-03-15 10:36:17 -07:00
  • 1a8570ed3f
    Refactor seq_nielsen: address NSB review comments (#8993) Copilot 2026-03-15 10:35:45 -07:00
  • 9256dd66e6
    Switch memory-safety workflow from push to weekly Monday schedule (#9001) Copilot 2026-03-15 10:26:10 -07:00
  • d9298af8b8 Replace push trigger with weekly Monday schedule in memory-safety.yml copilot-swe-agent[bot] 2026-03-15 17:15:31 +00:00
  • 4e42b006f0 Initial plan copilot-swe-agent[bot] 2026-03-15 17:14:38 +00:00