mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 18:29:23 +00:00
Code Activity
15703 commits 46 branches 52 tags 178 MiB
Commit graph

15703 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner
c2595b9bc8 #5379 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-06 18:58:27 +02:00
Nikolaj Bjorner
af5b2a4179 #5376 2021-07-06 16:44:44 +02:00
Nikolaj Bjorner
ca05c66847 #5376 2021-07-06 14:20:23 +02:00
Marc Mosko
8a33391708
Expose optimize.assertAndTrack to Java (#5387) 
Co-authored-by: Marc Mosko <mmosko@parc.com>
 2021-07-06 01:22:00 -07:00
Gabriel Radanne
0c7625cd26
Remove size argument in OCaml's Z3.mk_re_intersect (#5383) 
* Remove size argument in OCaml's `Z3.mk_re_intersect`

Passing the size as argument is unnecessary in OCaml, and that argument is abridged in all similar `Seq` functions. This applies the same pattern.

* Enable the ocaml documentation in Seq.

Turn all the comments into proper documentation comments.
 2021-07-06 01:21:04 -07:00
Nikolaj Bjorner
bdcfba1324 use sort* not ast* #5386 2021-07-06 10:19:17 +02:00
Nikolaj Bjorner
2a8d00d815 fix #5378 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-06 00:04:16 +02:00
Nikolaj Bjorner
e5aa02b8f5 fix #5382 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-05 19:30:03 +02:00
Nikolaj Bjorner
7255a2afd1 fix #5379 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-05 18:43:11 +02:00
Nikolaj Bjorner
d5c6abe14d #close 5363 
Force in-lining auxiliary functions so that model values can be used by SPACER to retrieve counter-examples. This fixes the issue of terminating without a trace. It does not address inefficiency involved with invoking satisfiability checks to retrieve models during trace construction.
 2021-06-22 16:24:00 -07:00
Nikolaj Bjorner
55daa2424c fix #5362 2021-06-22 12:26:27 -07:00
Nikolaj Bjorner
f3737f6831 #5361 2021-06-21 14:58:00 -07:00
Robert Jacobson
161d38397b
In src/sat/sat_local_search.*: Changed the return type of constraint_slack to int64_t instead of uint64_t to match the m_slack member of the constraint struct, which has type int64_t. (#5360) 2021-06-21 14:40:31 -07:00
Nikolaj Bjorner
45228bf8fb #5323 heap use after free 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-20 09:25:19 -07:00
Nikolaj Bjorner
ed9341e3b0 #5336 2021-06-19 22:22:56 -07:00
Nikolaj Bjorner
02644b5b71 #5336 2021-06-19 22:22:56 -07:00
Nikolaj Bjorner
8d37495b7c merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-19 22:22:41 -07:00
Nikolaj Bjorner
4a0a678e3f #5336 2021-06-19 22:21:45 -07:00
Nikolaj Bjorner
f7d1cce69a #5336 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-19 22:12:52 -07:00
Nikolaj Bjorner
2138ef2ad0 build 2021-06-17 11:26:12 -07:00
Nikolaj Bjorner
93a4939d49 #5336 2021-06-17 11:15:37 -07:00
Nikolaj Bjorner
2174bccdba #5336 2021-06-17 00:45:52 -05:00
Nikolaj Bjorner
d016cb1da5 #5336 2021-06-16 23:57:44 -05:00
Nikolaj Bjorner
9038dfd30d #5336 2021-06-16 23:27:26 -05:00
Nikolaj Bjorner
d73ceaddc7 #5336 2021-06-16 23:19:16 -05:00
Nikolaj Bjorner
0b3a8522ac #5336 2021-06-16 21:57:46 -05:00
Nikolaj Bjorner
1dedfe3164 #5336 2021-06-16 21:24:50 -05:00
Nikolaj Bjorner
df9084ba23 #5336 2021-06-16 19:12:50 -05:00