mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
16031 commits 49 branches 53 tags 182 MiB
Commit graph

16031 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
750c06e258 #5417 2021-07-18 10:21:42 -07:00
Nikolaj Bjorner
284d599788 #5323 
https://github.com/Z3Prover/z3/issues/5323#issuecomment-866503616
 2021-07-18 05:14:14 -07:00
Nikolaj Bjorner
cde3eac7be #5323 2021-07-18 13:45:21 +02:00
Nikolaj Bjorner
ce1c8ee9e3 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-18 12:32:27 +02:00
Nikolaj Bjorner
e0cb24867f Merge branch 'master' of https://github.com/z3prover/z3 2021-07-18 12:31:23 +02:00
Nikolaj Bjorner
f239aeb4d4 add consequences forcing character values to be digits 2021-07-18 12:30:56 +02:00
Margus Veanes
a19910c13d
added regex simplification rules ~() = .+ and .+* = .* (#5416) 2021-07-18 12:09:19 +02:00
Nikolaj Bjorner
36d265a32c na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-18 12:06:45 +02:00
Nikolaj Bjorner
0bfd24aae9 add comments 2021-07-18 12:05:52 +02:00
Nikolaj Bjorner
439e499dd3 note 2021-07-17 21:29:48 +02:00
Nikolaj Bjorner
6f2bf37268 #5336 missing theory variable creation in fpa_solver 2021-07-17 20:31:11 +02:00
Nikolaj Bjorner
b031fefbb9 #5336 - assertion violation in q_solver 2021-07-17 20:30:52 +02:00
CEisenhofer
0fa4b63d26
Added sbv2s (#5413) 
* Added sbv2s

* Fixed indention

Co-authored-by: Clemens Eisenhofer <Clemens.Eisenhofer@tuwien.ac.at>
 2021-07-16 17:58:28 +02:00
Nikolaj Bjorner
9e5dcf3ecb bound length of ubv2s 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-16 16:17:59 +02:00
Margus Veanes
8e9bc86c23
fixed bug #5343 and did some related optimizations (#5411) 2021-07-15 22:28:59 +02:00
Nikolaj Bjorner
c7a7d40a8f remove incorrect and inefficient default model conversion 2021-07-15 18:47:25 +02:00
Nikolaj Bjorner
0e066fef1f fix boundary cases reported by Clemens 2021-07-15 13:43:13 +02:00
Nikolaj Bjorner
79c261736b charsort 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-13 19:50:41 +02:00
Nikolaj Bjorner
97a035fd6d add char sort to .net 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-13 19:43:12 +02:00
Nikolaj Bjorner
1b648437b7 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-13 17:42:34 +02:00
Nikolaj Bjorner
a3010c8875 version inc, bvsort->bitvecsort 2021-07-13 17:14:47 +02:00
Nikolaj Bjorner
7ae78da850 adding access to characters over API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-13 15:56:08 +02:00
Nikolaj Bjorner
3a402ca2c1 Update release.yml for Azure Pipelines 2021-07-13 15:25:23 +02:00
Nikolaj Bjorner
75a5de99ca Update release.yml for Azure Pipelines 2021-07-13 15:24:19 +02:00
Nikolaj Bjorner
82e477ac02 bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-13 14:40:32 +02:00
Nikolaj Bjorner
0752b1385c add length axioms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-13 14:22:58 +02:00
Nikolaj Bjorner
a49a5b3a0b add release note for 4.8.12 prepare for addressing #5406 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-13 09:43:00 +02:00
Nikolaj Bjorner
34677e0e7c fix update of bb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-13 09:32:05 +02:00
Nikolaj Bjorner
e5c5caea45 add call to function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-13 09:19:20 +02:00
Nikolaj Bjorner
f74adb1ebd ubv2s step3 2021-07-12 17:15:08 +02:00
Nikolaj Bjorner
b6a3891ac4 str.from_ubv step2 2021-07-12 15:00:36 +02:00
Nikolaj Bjorner
1bc10cebc5 add ubv2s step 1 2021-07-12 12:53:00 +02:00
Nikolaj Bjorner
805bb58289 fix #5404 2021-07-12 12:35:24 +02:00
Nikolaj Bjorner
de8b2041e6 make bpp work with nullptr 2021-07-12 00:03:32 +02:00
Nikolaj Bjorner
4c53655be7 add z3doc build to release script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-11 23:26:48 +02:00
Nikolaj Bjorner
2ccfb1937d na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-11 23:20:19 +02:00
Nikolaj Bjorner
a4f4975092 #5336 2021-07-11 21:08:53 +02:00
Nikolaj Bjorner
cab1076514 #5336 2021-07-11 21:00:58 +02:00
Nikolaj Bjorner
18a76ab82c #5336 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-11 06:42:27 +02:00
Nikolaj Bjorner
10ad5bae21 increment version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-11 06:17:58 +02:00
Nikolaj Bjorner
e05f5ef6d1 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-11 06:15:27 +02:00
Nikolaj Bjorner
5fac396c2f simplify some verbose trace-stream 2021-07-11 06:15:27 +02:00
Nikolaj Bjorner
bc2e6ce037 Update release.yml for Azure Pipelines 2021-07-10 22:42:02 +02:00
Nikolaj Bjorner
66fc980154 add helper axioms for int2bv #5396 2021-07-10 17:13:16 +02:00
Nikolaj Bjorner
34885562e0 try without #!/bin/env python #5397 2021-07-10 15:20:56 +02:00
Nikolaj Bjorner
0f8d2d1d51 fix #5399 2021-07-10 14:47:51 +02:00
Nikolaj Bjorner
2973d3bdc1 fix #5392 2021-07-07 23:43:30 +02:00
Nikolaj Bjorner
897cbf347b fix #5381 2021-07-07 16:51:06 +02:00
Nikolaj Bjorner
29c6d42380 is-char is overloaded #5389 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-07 08:20:31 +02:00
Nikolaj Bjorner
4f184b6aa9 fix #5376 2021-07-06 19:20:35 +02:00