3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Commit graph

8161 commits

Author SHA1 Message Date
Nikolaj Bjorner
470e49afc1
Merge pull request #1631 from JoranHonig/master
Parallel python example
2018-05-19 11:08:23 -07:00
Joran Honig
e32dfad81e Add comments 2018-05-19 11:16:20 +02:00
Joran Honig
7d51353b8b Implement parallel python example 2018-05-19 11:13:53 +02:00
Nikolaj Bjorner
ad973d5c6d Merge branch 'master' of https://github.com/z3prover/z3 2018-05-18 14:31:16 -07:00
Nikolaj Bjorner
4b3483ec6e Merge branch 'master' of https://github.com/z3prover/z3 2018-05-18 14:30:35 -07:00
Nikolaj Bjorner
d462ed3f00 fix #1621
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-18 14:30:27 -07:00
Nikolaj Bjorner
8302360321 fix #1625
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-18 14:24:12 -07:00
Nikolaj Bjorner
925867dc3e fix #1621
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-18 14:14:00 -07:00
Nikolaj Bjorner
e5b14ab682 fix #1625
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-18 14:03:32 -07:00
Nikolaj Bjorner
2c71640503
Merge pull request #1624 from sb98052/master
Link in Big_int via num package
2018-05-17 20:58:30 -07:00
Sapan Bhatia
c198b12743 Big_int is no longer a part of OCaml's standard library and must be
included via the num package: https://github.com/ocaml/num
2018-05-15 04:55:57 +05:30
Nikolaj Bjorner
a6829ea9d0 Merge branch 'master' of https://github.com/z3prover/z3 2018-05-13 05:40:56 -07:00
Nikolaj Bjorner
53976d0ddf
Merge pull request #1613 from corrodedHash/master
Fixed Segfault when failing to load datalog file
2018-05-08 18:55:35 +01:00
corrodedHash
d097d90731 Fixed Segfault when failing to load datalog file 2018-05-08 19:26:14 +02:00
Nikolaj Bjorner
bc3719f436
Merge pull request #1612 from danielschemmel/gcc8
`lp::permutation_matrix::values` attempts an incorrect conversion
2018-05-08 15:49:22 +01:00
Daniel Schemmel
2d5dd80238
The Permutation Matrix' values function attempted an incorrect conversion.
This causes compilation with GCC 8 to fail. I suspect it worked previously due to SFINAE.
2018-05-07 23:33:40 +02:00
Nikolaj Bjorner
502d0e37dd
Merge pull request #1611 from Z3Prover/revert-1610-cv/encoding
Revert "Specify encoding of source files in mk_util.py"
2018-05-03 12:00:03 -07:00
Nikolaj Bjorner
888699548d
Revert "Specify encoding of source files in mk_util.py" 2018-05-03 11:59:49 -07:00
Nikolaj Bjorner
c293d325a9
Merge pull request #1610 from varming/cv/encoding
Specify encoding of source files in mk_util.py
2018-05-03 11:51:37 -07:00
Nikolaj Bjorner
6e03c7a542 fix #1607 by filtering exceptions when the context is canceled
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-03 03:23:54 -07:00
Carsten Varming
c279fd9f2e Specify encoding of source files in mk_util.py 2018-05-02 23:27:33 -04:00
Nikolaj Bjorner
6bff15e12e fix #1609
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-02 10:38:46 -07:00
Nikolaj Bjorner
fd5159bf18 Merge branch 'master' of https://github.com/z3prover/z3 2018-05-01 07:13:05 -07:00
Nikolaj Bjorner
371880da04 n/a
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-01 07:13:03 -07:00
Nikolaj Bjorner
b8193a0ae6 fix #1604
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-29 10:04:42 -07:00
Nikolaj Bjorner
c64d044e60 Merge branch 'master' of https://github.com/z3prover/z3 2018-04-27 17:49:51 +02:00
Nikolaj Bjorner
f234bb348b fix #1599. fix #1600
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-27 17:49:20 +02:00
Nikolaj Bjorner
5dbba8bd53 fix #1599. fix #1600
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-27 17:48:04 +02:00
Nikolaj Bjorner
a9568d1b12
Merge pull request #1597 from TheRealNebus/master
WMax Bug Fix
2018-04-27 09:53:29 +02:00
Nikolaj Bjorner
b5c77065e9
Merge pull request #1596 from mtrberzi/develop
fix memory leak related to #1575
2018-04-27 09:52:50 +02:00
TheRealNebus
24b35fb925 WMax conflict budget bug fix 2018-04-26 22:42:55 +01:00
TheRealNebus
e1d7f5deba Revert "MSS based MaxSMT solver"
This reverts commit 3bbc09c1d2.
2018-04-26 22:40:00 +01:00
TheRealNebus
7e8ed0762d Revert "implemented CLD"
This reverts commit 3a7efb91ae.
2018-04-26 22:39:58 +01:00
TheRealNebus
bf2a031f7b Revert "disjoint cores"
This reverts commit e5aa79ba6a.
2018-04-26 22:39:55 +01:00
TheRealNebus
37852807b0 Revert "WMax conflict budget bug fix"
This reverts commit ab8d3cdc44.
2018-04-26 22:39:45 +01:00
Murphy Berzish
047f6c558c fix memory leak related to #1575 2018-04-26 16:36:14 -04:00
Nikolaj Bjorner
74292a48e5 change order of concatentation for empty string, #1595
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-26 09:08:34 +02:00
Nikolaj Bjorner
a04921dafe fix #1595
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-26 08:47:05 +02:00
Nikolaj Bjorner
cf2258a536 fix #1594
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-26 08:39:35 +02:00
Nikolaj Bjorner
f54779fe09 Merge branch 'master' of https://github.com/z3prover/z3 2018-04-25 11:18:39 +02:00
Nikolaj Bjorner
b5f067bec5 fix #1592 #1587
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-25 11:18:24 +02:00
TheRealNebus
ab8d3cdc44 WMax conflict budget bug fix 2018-04-24 17:59:21 +01:00
Nikolaj Bjorner
484d20c1f2
Merge pull request #1591 from yxliang01/master
Z3 now will also try to find libz3 in PYTHONPATH
2018-04-24 17:23:27 +02:00
yxliang01
f7bcf0fd58 Z3 now will also try to find libz3 in PYTHONPATH 2018-04-24 08:17:20 -07:00
Christoph M. Wintersteiger
e13f3d92af Updated CMakelists.txt 2018-04-24 15:01:05 +01:00
Christoph M. Wintersteiger
2e3c335e14 Merge branch 'master' of https://github.com/Z3Prover/z3 2018-04-24 12:43:14 +01:00
Christoph M. Wintersteiger
a1d870f19f Added tactic for QF_FPLRA 2018-04-24 12:43:11 +01:00
Nikolaj Bjorner
e3a40459bf
Merge pull request #1588 from bannsec/z3_nonascii_encoding
Fancy dots are not allowed here!!
2018-04-24 08:34:50 +02:00
bannsec
5166b96d20 Fancy dots are not allowed here!! 2018-04-23 17:17:51 -04:00
Nikolaj Bjorner
19bb883263 fix #1581
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-23 12:12:39 +02:00