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

14996 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
5f9973d8c4 fix #4508 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-07 16:28:53 -07:00
Nikolaj Bjorner
d2a12f6db5 tuning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-07 12:52:13 -07:00
FabianWolff
cfed69caae
Remove __DATE__ to make the build more reproducible (#4505) 2020-06-07 12:28:39 -07:00
FabianWolff
30a3618ebf
Fix build failure on riscv64 (#4506) 2020-06-07 12:27:54 -07:00
Nuno Lopes
1809ee5107 fix regression in FPA internalization 2020-06-07 15:50:53 +01:00
Nikolaj Bjorner
ba1ca33637 normalization of union/intersection 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-06 12:54:44 -07:00
Nikolaj Bjorner
ccea27de35 add nullable propagation instead of waiting for length assignment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-06 12:11:04 -07:00
Nikolaj Bjorner
65b6ccd651 add nullable propagation instead of waiting for length assignment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-06 11:32:43 -07:00
Nikolaj Bjorner
1b9fcc7098 integrate ite-normalized derivatives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-05 17:28:48 -07:00
Nikolaj Bjorner
4dbf7b183d inline conditions with derivative computation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-05 13:51:31 -07:00
Nikolaj Bjorner
a32fabf5ee fix #4403 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-05 13:51:31 -07:00
Andrew V. Jones
bb9cd5dd49
Ensure that the 'OUTPUT' locations in CMake for Python examples is accurate (#4499) 
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
 2020-06-04 15:04:01 -07:00
Nikolaj Bjorner
59e388ece1 handle bind proof constructor and print lambda 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-04 11:59:59 -07:00
Nikolaj Bjorner
e52eed325c close #4450 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-04 09:22:38 -07:00
Nikolaj Bjorner
57086edc42 close #4432 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-04 03:06:58 -07:00
Nikolaj Bjorner
f999c14a1e close #4429 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-04 01:33:28 -07:00
Nikolaj Bjorner
278e004385 fix #4428, and then there were none, almost 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-04 01:28:26 -07:00
Nikolaj Bjorner
80d5d66158 handling cancelation #4425 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-04 01:12:04 -07:00
Nikolaj Bjorner
9f8887cc2e throw from push #4425 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-04 01:05:23 -07:00
Nikolaj Bjorner
b013df9a9f fix #4431 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-04 00:47:27 -07:00
Nikolaj Bjorner
b29d5f9b5d fix #4436 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 21:21:01 -07:00
Nikolaj Bjorner
9ca5b3f304 fix #4449 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 21:10:07 -07:00
Nikolaj Bjorner
cbf089e10d fix #4448 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 19:41:25 -07:00
Nikolaj Bjorner
ae2f0ca85b fix #4448 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 19:40:26 -07:00
Nikolaj Bjorner
743573aac5 fix #4447, or mask it 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 19:32:05 -07:00
Nikolaj Bjorner
af90992858 fix #4404 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 17:01:36 -07:00
Nikolaj Bjorner
f986ae97bd fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 15:12:08 -07:00
Nikolaj Bjorner
d50fc6976b fix #4430 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 13:47:59 -07:00
Andrew V. Jones
9fac010d8e
Fixing build errors when building test-z3 (#4496) 
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
 2020-06-03 13:34:43 -07:00
Nuno Lopes
e844aef896 remove a few more copy constructors, though still not enough to enable the assertion in vector 
I give up for now; there are too many copies left for little return..
 2020-06-03 20:32:13 +01:00
Nikolaj Bjorner
e2b2b7f82e na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 12:29:29 -07:00
Nikolaj Bjorner
3a7df2c6ef fix various nullability checks in seq_regex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 12:28:32 -07:00
Nikolaj Bjorner
377dbad3b9 fix #4435 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 10:27:08 -07:00
Nikolaj Bjorner
8ae42b5ae1 fix #4433 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 10:23:26 -07:00
Nikolaj Bjorner
f5cd4e3ac0 janitor services 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 10:15:55 -07:00
Nikolaj Bjorner
38176256c4 fix #4434 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 10:12:49 -07:00
Nikolaj Bjorner
6e47499e26 fix #4434 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 10:09:18 -07:00
Andrew V. Jones
a23ca1792b
Ensure that Z3 uses the correct SMT-LIB2 syntax for push and pop (#4495) 
* When pretty-printing SMTLIB2, ensure that Z3 uses the correct syntax for 'push'

Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>

* When pretty-printing SMTLIB2, ensure that Z3 uses the correct syntax for 'pop'

Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
 2020-06-03 09:35:14 -07:00
Nikolaj Bjorner
0bc33e9c9d correct the type returned by mkNth #4454 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 09:10:58 -07:00
Nuno Lopes
7ac2791482 remove a bunch of constructors to avoid copies 
still not enough to guarantee that vector::expand doesnt copy (WIP)
 2020-06-03 17:09:27 +01:00
Nuno Lopes
98b5abb1d4 buffer: require a move constructor to avoid copies 
remove unneded copy constructors from several classes
 2020-06-03 11:57:49 +01:00
Nuno Lopes
3d98bccc33 fix mem leak in buffer and remove copies in interval (#4458) 2020-06-03 10:26:00 +01:00
Nikolaj Bjorner
04829e6b7a fix #4437, not really interesting bug as debug assertion is really for non-interrupted flow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-02 18:41:26 -07:00
Nikolaj Bjorner
df75792e9c fix #4454 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-02 18:35:38 -07:00
Nikolaj Bjorner
3f2dafe047 fix $4457 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-02 18:32:01 -07:00
Nikolaj Bjorner
d3e20d41b2 fix $4457 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-02 18:31:28 -07:00
Nikolaj Bjorner
f645ef7677 fix #4461 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-02 18:08:42 -07:00
Nikolaj Bjorner
bfb5c95b9a use op-cache for is-nullable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-02 13:30:18 -07:00
Nikolaj Bjorner
e388055a33 connecting op-cache 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-02 13:13:32 -07:00
Nikolaj Bjorner
320cd81140 fix #4476 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-02 13:00:55 -07:00