3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00

Commit graph

  • ac6554eb92 set C++ version to 20 Nikolaj Bjorner 2024-03-21 10:59:31 -07:00
  • 182979771f disable verbose Nikolaj Bjorner 2024-03-21 10:35:13 -07:00
  • 648e05754c #7178 copy build tool chains used for manylinux arm64 into ubuntu builds Nikolaj Bjorner 2024-03-21 09:40:50 -07:00
  • 6455de9dd3 fix #7179 Nikolaj Bjorner 2024-03-21 09:39:13 -07:00
  • 934b2ad5ef update target selection to what was intended Jakob Rath 2024-03-21 13:53:26 +01:00
  • 342db52558 fix Jakob Rath 2024-03-21 12:03:52 +01:00
  • acd05686e4 relevant level should be based on what's to appear in the lemma Jakob Rath 2024-03-21 11:05:55 +01:00
  • 530c6fc625 fix ##7175 - don't add user macros/functions when smtlib2_compliant=true Nikolaj Bjorner 2024-03-20 22:05:30 -07:00
  • 27a9b8bd03 fix project minor version Nikolaj Bjorner 2024-03-20 21:32:18 -07:00
  • f840d5d965 na Nikolaj Bjorner 2024-03-20 21:27:00 -07:00
  • 70d2263a85 cast, updated nlexplain Nikolaj Bjorner 2024-03-19 12:29:55 -07:00
  • 730f9ad9b7 Nikolaj's fix in add_zero_assumption Lev Nachmanson 2024-03-19 09:42:36 -10:00
  • 7d1a57b6e9 remove commented code Jakob Rath 2024-03-20 15:38:22 +01:00
  • 7922ee3e82 debug output Jakob Rath 2024-03-20 15:37:34 +01:00
  • fd9c931168 skip entry for origin variable Jakob Rath 2024-03-20 15:37:03 +01:00
  • 23ca9d9fc5 select targets, try generic/specific version of projection Jakob Rath 2024-03-20 15:26:33 +01:00
  • de809932eb refactor, minor fixes Jakob Rath 2024-03-20 14:33:30 +01:00
  • ef6b5f82d1 relax level constraint Jakob Rath 2024-03-20 13:39:16 +01:00
  • 91a9feb5a8 warnings Jakob Rath 2024-03-20 12:16:24 +01:00
  • f47fbdd714 Move interval projection out of viable Jakob Rath 2024-03-20 12:10:19 +01:00
  • a9054bc73b
    fix warning C4244 in util.h (#7171) 向阳 2024-03-20 17:31:23 +08:00
  • 5339a2f70f Don't access solver_interface directly Jakob Rath 2024-03-20 10:16:40 +01:00
  • a34bb99db3 Use variable from violated interval as origin Jakob Rath 2024-03-20 10:15:25 +01:00
  • 3a11350142 Move helper functions Jakob Rath 2024-03-20 10:10:27 +01:00
  • bee6c7f6ad
    Update util.h - fix warning C4244 向阳 2024-03-20 14:54:44 +08:00
  • 6eeb022048 fix encoding for sdiv exposed by zQkAOXjEDwgm Nikolaj Bjorner 2024-03-19 16:00:09 -07:00
  • ffe7b46e74 unsigned cast Nikolaj Bjorner 2024-03-19 15:02:42 -07:00
  • db5f2767cd Nikolaj's fix in add_zero_assumption Lev Nachmanson 2024-03-19 09:42:36 -10:00
  • f5eb457bee fix propagate_from_containing_slice dependency Jakob Rath 2024-03-19 16:13:28 +01:00
  • 489a1495d2 dep Jakob Rath 2024-03-19 14:23:44 +01:00
  • adc5313916 remove debug output Jakob Rath 2024-03-19 10:11:06 +01:00
  • 148eafaaf0 Merge remote-tracking branch 'origin/master' into poly Jakob Rath 2024-03-19 09:50:24 +01:00
  • 1a7437144c
    Bump docker/build-push-action from 5.2.0 to 5.3.0 (#7170) dependabot[bot] 2024-03-18 15:25:58 -07:00
  • ee20693593
    Bump docker/build-push-action from 5.2.0 to 5.3.0 dependabot[bot] 2024-03-18 22:10:46 +00:00
  • 18365907a2
    Update util.h (#7169) cctv130 2024-03-18 11:29:27 +08:00
  • 1a6b4cd098
    Update util.h cctv130 2024-03-18 10:35:37 +08:00
  • b8a69987c3 fix #7165 Nikolaj Bjorner 2024-03-17 16:33:32 -07:00
  • fb824bee54 inline unfolding if it is linear or constant. Nikolaj Bjorner 2024-03-16 13:02:26 -07:00
  • 3555b25317 Merge branch 'poly' of https://github.com/z3prover/z3 into poly Nikolaj Bjorner 2024-03-15 08:55:16 -07:00
  • e4cc6e29ca fix case when interval is full Nikolaj Bjorner 2024-03-15 08:55:07 -07:00
  • aa1285288e Fix integration of propagate_from_containing_slice Jakob Rath 2024-03-15 15:08:12 +01:00
  • dfb200a3c9 propagation from containing slice depends on concrete values Jakob Rath 2024-03-15 12:31:31 +01:00
  • 6450a7a0b8
    Bump docker/build-push-action from 5.1.0 to 5.2.0 (#7159) dependabot[bot] 2024-03-14 16:54:01 -07:00
  • 5704e8d154
    fix intblast is_bounded (#7163) Jakob Rath 2024-03-14 16:48:38 +01:00
  • 2102db2df8 Fix viable entry reduction (case new_lo == new_hi) Jakob Rath 2024-03-14 15:09:21 +01:00
  • f6c99585f3 fix warning Jakob Rath 2024-03-14 15:08:00 +01:00
  • f56a89f2d1 fix intblast is_bounded Jakob Rath 2024-03-13 12:37:37 +01:00
  • 82dc254d0e Merge branch 'poly' of https://github.com/z3prover/z3 into poly Nikolaj Bjorner 2024-03-13 16:20:54 -07:00
  • c2f8dd9a02 use -> types Nikolaj Bjorner 2024-03-13 16:20:51 -07:00
  • 1f0a6c051a update slice/offset claim structures to allow for equal variable. Nikolaj Bjorner 2024-03-13 11:49:11 -07:00
  • 1e9381c2f6 update slice/offset claim structures to allow for equal variable. Nikolaj Bjorner 2024-03-13 11:48:09 -07:00
  • 5d1602b6c7 print validation failures Jakob Rath 2024-03-13 14:12:10 +01:00
  • 7da7e99ca2 try_umul_blast Jakob Rath 2024-03-13 14:01:07 +01:00
  • 8a16631fd1 fix intblast is_bounded Jakob Rath 2024-03-13 12:37:37 +01:00
  • d07d57c240 remove leftovers from earlier commit Jakob Rath 2024-03-13 09:42:08 +01:00
  • 22d80277ae signed_constraint == Jakob Rath 2024-03-12 16:26:27 +01:00
  • 35e3211ca8 display Jakob Rath 2024-03-12 16:24:28 +01:00
  • 450ed26440 implement 'is_full' case Jakob Rath 2024-03-12 16:23:23 +01:00
  • df85eeb581 viable explanation depends on assignment Jakob Rath 2024-03-12 16:20:44 +01:00
  • 58c14ba2f9 write validation in bv format too Jakob Rath 2024-03-12 16:18:39 +01:00
  • 37bf5fefca fix extract axiom Jakob Rath 2024-03-12 13:47:23 +01:00
  • 0b3bbc2972 #7158 Nikolaj Bjorner 2024-03-11 18:19:36 -07:00
  • 230d19ed95
    Bump docker/build-push-action from 5.1.0 to 5.2.0 dependabot[bot] 2024-03-11 22:51:26 +00:00
  • 7311af699c fix Jakob Rath 2024-03-11 15:02:55 +01:00
  • d11c2b3265 Add ule_constraint simplification Jakob Rath 2024-03-11 14:19:35 +01:00
  • 2fdf2233f9 move side effect out of print statement Nikolaj Bjorner 2024-03-11 04:08:07 -07:00
  • 7bbe3fb2b6
    fix (get-proof) command to respect option pp.simplify_implies (#7157) someplaceguy 2024-03-09 23:13:42 +00:00
  • 593be8984c fix (get-proof) command to respect option pp.simplify_implies someplaceguy 2024-03-09 21:21:39 +00:00
  • 361e04a18e port fixes to intblast Nikolaj Bjorner 2024-03-09 10:27:12 -08:00
  • e8ac3aa88c port fixes to intblast Nikolaj Bjorner 2024-03-09 09:43:14 -08:00
  • dcaacf5e9b add rewrite glue for instantiating equalities, #7154 Nikolaj Bjorner 2024-03-07 15:21:26 -08:00
  • a4ecaf1ff5 increment version number Nikolaj Bjorner 2024-03-07 11:22:08 -08:00
  • 3049f578a8 add download of Arm64 to python packaging z3-4.13.0 Nikolaj Bjorner 2024-03-07 10:25:16 -08:00
  • f9ce332b54 update release notes Nikolaj Bjorner 2024-03-07 09:15:34 -08:00
  • 6254844e2d update release notes Nikolaj Bjorner 2024-03-07 09:14:34 -08:00
  • 7b7084d373
    Add LinuxBuildsArm64 to python wheels in release (#7155) Steven Moy 2024-03-07 09:11:47 -08:00
  • 5bf6367ab1 Add LinuxBuildsArm64 to python wheels in release Steven Moy 2024-03-07 09:08:33 -08:00
  • e873664fe8
    Downgrade arm cross compile toolchain to glibc 2.34 (#7153) Steven Moy 2024-03-06 20:14:06 -08:00
  • 712a90759e Downgrade arm cross compile toolchain to glibc 2.34 Steven Moy 2024-03-06 16:23:48 -08:00
  • 364da19122 remove test Nikolaj Bjorner 2024-03-06 13:54:28 -08:00
  • 620efbb67b add aacrhc Nikolaj Bjorner 2024-03-06 13:53:43 -08:00
  • aad8cbdd9d
    Add LinuxBuildsArm64 ci azure-pipelines for testing (#7152) Steven Moy 2024-03-06 13:21:17 -08:00
  • a924e0318d Add LinuxBuildsArm64 ci azure-pipelines for testing Steven Moy 2024-03-06 10:54:04 -08:00
  • 017367d7af
    Handle cross compile within manylinux (#7150) Steven Moy 2024-03-06 08:27:04 -08:00
  • 08abf71abb Handle cross compile within manylinux Steven Moy 2024-03-05 22:17:53 -08:00
  • e8c8d8aa7d
    Put in workaround to rename manylinux_arm64 to manylinux_aarch64 (#7149) Steven Moy 2024-03-05 13:38:12 -08:00
  • 7aaa5a8da2 Put in workaround to rename manylinux_arm64 to manylinux_aarch64 Steven Moy 2024-03-05 13:35:13 -08:00
  • d6f522e205 na Nikolaj Bjorner 2024-03-05 02:53:47 -08:00
  • 531bda39ac fix alias bug Nikolaj Bjorner 2024-03-02 10:15:14 -08:00
  • 657aaf9a0f na Nikolaj Bjorner 2024-03-02 10:15:44 -08:00
  • 8679c08010 fix test Nikolaj Bjorner 2024-03-01 03:42:58 -08:00
  • 22616da63b updates Nikolaj Bjorner 2024-02-29 16:59:03 -08:00
  • 5be8872d6a na Nikolaj Bjorner 2024-02-29 08:54:21 -08:00
  • dfd5c27fec na Nikolaj Bjorner 2024-02-28 17:09:41 -08:00
  • 803f0f0c65 na Nikolaj Bjorner 2024-02-28 17:22:20 +00:00
  • 5455603910 na Nikolaj Bjorner 2024-02-28 08:57:54 -08:00
  • 9888d87294 na Nikolaj Bjorner 2024-02-27 07:06:05 -08:00
  • f46c3782d6 bugfixes Nikolaj Bjorner 2024-02-26 19:49:37 -08:00
  • d774f07eb3 add eval field to sls-valuation to track temporary values. Nikolaj Bjorner 2024-02-26 14:54:15 -08:00
  • 8f139e862c updates to multiplication Nikolaj Bjorner 2024-02-26 08:16:12 -08:00