mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-17 22:35:35 +00:00
Code Activity
15454 commits 23 branches 48 tags 157 MiB
Commit graph

15454 commits

Author SHA1 Message Date
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 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 2021-07-11 21:08:53 +02:00
Nikolaj Bjorner cab1076514 2021-07-11 21:00:58 +02:00
Nikolaj Bjorner 18a76ab82c 
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 2021-07-10 17:13:16 +02:00
Nikolaj Bjorner 34885562e0 try without #!/bin/env python 2021-07-10 15:20:56 +02:00
Nikolaj Bjorner 0f8d2d1d51 fix 2021-07-10 14:47:51 +02:00
Nikolaj Bjorner 2973d3bdc1 fix 2021-07-07 23:43:30 +02:00
Nikolaj Bjorner 897cbf347b fix 2021-07-07 16:51:06 +02:00
Nikolaj Bjorner 29c6d42380 is-char is overloaded 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-07 08:20:31 +02:00
Nikolaj Bjorner 4f184b6aa9 fix 2021-07-06 19:20:35 +02:00
Nikolaj Bjorner c2595b9bc8 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-06 18:58:27 +02:00
Nikolaj Bjorner af5b2a4179 2021-07-06 16:44:44 +02:00
Nikolaj Bjorner ca05c66847 2021-07-06 14:20:23 +02:00
Marc Mosko 8a33391708
Expose optimize.assertAndTrack to Java () 
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 () 
* 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* 2021-07-06 10:19:17 +02:00
Nikolaj Bjorner 2a8d00d815 fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-06 00:04:16 +02:00
Nikolaj Bjorner e5aa02b8f5 fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-05 19:30:03 +02:00
Nikolaj Bjorner 7255a2afd1 fix 
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 2021-06-22 12:26:27 -07:00
Nikolaj Bjorner f3737f6831 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. () 2021-06-21 14:40:31 -07:00
Nikolaj Bjorner 45228bf8fb heap use after free 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-20 09:25:19 -07:00
Nikolaj Bjorner ed9341e3b0 2021-06-19 22:22:56 -07:00
Nikolaj Bjorner 02644b5b71 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 2021-06-19 22:21:45 -07:00
Nikolaj Bjorner f7d1cce69a 
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 2021-06-17 11:15:37 -07:00
Nikolaj Bjorner 2174bccdba 2021-06-17 00:45:52 -05:00
Nikolaj Bjorner d016cb1da5 2021-06-16 23:57:44 -05:00
Nikolaj Bjorner 9038dfd30d 2021-06-16 23:27:26 -05:00
Nikolaj Bjorner d73ceaddc7 2021-06-16 23:19:16 -05:00
Nikolaj Bjorner 0b3a8522ac 2021-06-16 21:57:46 -05:00
Nikolaj Bjorner 1dedfe3164 2021-06-16 21:24:50 -05:00