mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity
15838 commits 23 branches 48 tags 157 MiB
Commit graph

15838 commits

Author SHA1 Message Date
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
Nikolaj Bjorner df9084ba23 2021-06-16 19:12:50 -05:00
Nikolaj Bjorner 3311bd074f 2021-06-16 18:42:44 -05:00
Nikolaj Bjorner 6b5680f13e 2021-06-16 18:42:19 -05:00
Nikolaj Bjorner 38fc97d18c 2021-06-16 17:47:49 -05:00
Nikolaj Bjorner 29a2838bc9 2021-06-16 16:01:42 -05:00
Nikolaj Bjorner f95d0b7216 2021-06-16 16:01:42 -05:00
Nikolaj Bjorner fbc3aa93a5 2021-06-16 16:01:42 -05:00
Gram 589f99eea9
Fix Flake8 violations in Python API () 
* Fix flake8 violations in z3.py

* Fix flake8 violations in z3printer.py

* Fix flake8 violations in z3rcf.py and z3util.py

* do not allocate list on every call to set_default_rounding_mode
 2021-06-16 10:49:47 -05:00
Iain Scott d61d5081a2
Delete unused NuGet release script. () 2021-06-16 10:48:51 -05:00
Nikolaj Bjorner dc6a8fde34 fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-15 13:53:22 -05:00
Nikolaj Bjorner 9c6b29164d 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-15 12:31:40 -05:00
Nikolaj Bjorner 206d7709d3
Update README.md 2021-06-15 12:25:03 -05:00
Nikolaj Bjorner 082ec0f499 2021-06-08 20:03:03 -07:00
Nikolaj Bjorner 08b4c4ea14 2021-06-08 19:48:05 -07:00
Nikolaj Bjorner fb6cd8e132 2021-06-08 15:15:02 -07:00
Nikolaj Bjorner bdf6a17b89 2021-06-08 13:37:29 -07:00