mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity
16381 commits 23 branches 48 tags 156 MiB
Commit graph

16381 commits

This branch
This branch
All branches
Author SHA1 Message Date
Andreas 4f4e9a9963
fix a tiny typo (#5960) 
A dot.
 2022-04-11 08:40:03 +02:00
Clemens Eisenhofer 0b20a4ebf4
Added rewriting distinct with bitvectors to false if bit-size is too low (#5956) 
* Fixed problem with registering bitvector functions

* Added rewriting distinct with bitvectors to false if bit-size is too low

* Removed debug output

* Incorporated Nikolaj's comments

* Simplifications
 2022-04-09 21:46:21 +02:00
Nikolaj Bjorner f55b233228 #5778 2022-04-09 12:06:39 +02:00
Nikolaj Bjorner 011c1b2dd2 remove refs to bare_str 2022-04-09 12:06:27 +02:00
Nikolaj Bjorner 405a26c585 allow adding constraints during on_model 2022-04-09 09:55:02 +02:00
Nikolaj Bjorner 005b8e3cf8 arc -> arch 2022-04-09 08:28:22 +02:00
Nikolaj Bjorner fe834b9e4e update regex 2022-04-09 07:40:48 +02:00
Nikolaj Bjorner c98eda03f7 nightly osx arm64 wheel 2022-04-09 06:55:31 +02:00
Nikolaj Bjorner d6d9b25c68 Allow adding constraints in the model_eh callback 2022-04-08 17:12:20 +02:00
Nikolaj Bjorner fbd35fb58d skip unit tests for arm 2022-04-08 16:55:39 +02:00
Nikolaj Bjorner 91ca02864c arm64 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-08 14:59:22 +02:00
Nikolaj Bjorner 3821eb4134 fpflags 2022-04-08 14:47:38 +02:00
Nikolaj Bjorner f3789e21a3 id doesn't use mk_util 2022-04-08 14:42:18 +02:00
Nikolaj Bjorner 67434a3096 again 2022-04-08 14:40:55 +02:00
Nikolaj Bjorner 9533dbaf5c missing arg specifier 2022-04-08 14:34:52 +02:00
Nikolaj Bjorner 746a4161af more passing of parameters 2022-04-08 14:24:21 +02:00
Nikolaj Bjorner cb6aba2315 more arm 2022-04-08 14:07:56 +02:00
Nikolaj Bjorner 79553261d1 no uname on nt 2022-04-08 07:02:32 +02:00
Nikolaj Bjorner 1346a168a1 #5952 2022-04-08 07:00:53 +02:00
Nikolaj Bjorner babac78c99 syntax error? 2022-04-08 06:59:07 +02:00
Nikolaj Bjorner 83d2aa85ec add arm64 build path 2022-04-08 06:35:25 +02:00
Nikolaj Bjorner 2e91d66888 Update mk_util.py 
use more meaningful name
 2022-04-08 06:28:36 +02:00
Nikolaj Bjorner c47bd1d01f add arm64 auto-detect 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-07 13:43:35 +02:00
Nikolaj Bjorner 8c2909f52b working on python make for arm 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-07 13:36:23 +02:00
Nikolaj Bjorner 1953165422 set ARM64 if detected under OSX 2022-04-07 08:35:56 +02:00
fleisherdev a863a91b13
Allow nightly builds to complete even if package signing fails - NOT published to nuget.org (#5951) 
Co-authored-by: jofleish <jofleish@microsoft.com>
 2022-04-07 08:19:21 +02:00
Nikolaj Bjorner 0fa0feb979 allow add_expr during pop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-06 16:27:10 +02:00
Nikolaj Bjorner b0dce5b27d remove debug asserts 2022-04-06 08:53:12 +02:00
Nikolaj Bjorner 2f63747c7b #5778 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-06 08:17:27 +02:00
Nikolaj Bjorner cebbc71330 #5778 ensure else value so that defaults align across equivalence class 2022-04-06 07:58:32 +02:00
fleisherdev ac2523af82
Fix null ref on access of Entry[] contents (#5947) 
Co-authored-by: jfleisher <jofleish@microsoft.com>
 2022-04-06 05:37:51 +02:00
Nikolaj Bjorner bd70c79b25 Update target_arch_detect.cpp 
adding detection for ARM to cmake build
 2022-04-05 15:53:53 +02:00
Nikolaj Bjorner a5d588ce09 add example for #5933 2022-04-05 04:26:40 +02:00
Nikolaj Bjorner 053cb72cc2 handle return status 2022-04-04 20:19:15 +02:00
Nikolaj Bjorner 4f6811a6a2 with simplification 2022-04-03 21:10:53 -07:00
Nikolaj Bjorner 05ec77cb56 revert 2022-04-03 12:20:10 -07:00
Nikolaj Bjorner 321745fdb1 #5941 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-03 11:07:54 -07:00
Nikolaj Bjorner 03a2d9a018 fix #5942 2022-04-03 11:03:28 -07:00
Nikolaj Bjorner 46cc54fbab outdated warning 2022-04-03 07:55:51 -07:00
Nikolaj Bjorner 34272152bb add stubs to control memory usage 2022-04-02 17:52:54 -07:00
Nikolaj Bjorner 4b495e4b96 nits 2022-04-02 17:50:45 -07:00
Nikolaj Bjorner d0ef5948aa nits 2022-04-02 17:49:03 -07:00
Nikolaj Bjorner 25feb0ebed #5938 catch also rewriter_exception that can be raised on cancelation and memory pressure 2022-04-02 17:43:12 -07:00
Nikolaj Bjorner ef28f0e2f0 #5778 
deal with recursive calls to internalization with the same formula
 2022-04-02 01:28:58 -07:00
Nikolaj Bjorner 2fedcbd41e #5778 2022-04-02 01:27:56 -07:00
Nikolaj Bjorner 229ea569f1 #5778 2022-04-02 00:56:51 -07:00
Nikolaj Bjorner 97115e5ebd #5778 
add new clauses created during propagation to use-list
 2022-04-02 00:14:59 -07:00
Nikolaj Bjorner 4cc33277fa #5778 2022-04-01 14:27:40 -07:00
Nikolaj Bjorner c7922d69ac #5778 2022-04-01 14:17:45 -07:00
Nikolaj Bjorner 81084b8232 #5778 #5937 2022-04-01 13:07:17 -07:00