Nikolaj Bjorner
|
7255edf216
|
remove new_sub
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-06 17:13:59 -07:00 |
|
Nikolaj Bjorner
|
44b0b0148b
|
deal with warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-06 17:13:38 -07:00 |
|
Nikolaj Bjorner
|
e731a44880
|
Merge pull request #2329 from Z3Prover/nomp
Nomp
|
2019-06-07 02:05:11 +02:00 |
|
Nikolaj Bjorner
|
82da3493ee
|
fix printing of recursive defs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-06 13:11:46 -07:00 |
|
Nikolaj Bjorner
|
71009a9d02
|
suspend limits during assert and macro expansion
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-06 11:07:57 -07:00 |
|
Nikolaj Bjorner
|
7c1e935bc2
|
rlimit mux
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-05 22:17:09 -07:00 |
|
Nikolaj Bjorner
|
fdfb9e4fd5
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2019-06-05 16:10:31 -07:00 |
|
Nikolaj Bjorner
|
aabc54409c
|
change printing directires
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-05 16:10:22 -07:00 |
|
Nikolaj Bjorner
|
a8b02ddb93
|
fix #2323
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-05 13:43:45 -07:00 |
|
Nikolaj Bjorner
|
1ca3381390
|
fix #2319
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-05 09:42:19 -07:00 |
|
Nuno Lopes
|
a53ff6f21c
|
turn locks into no-ops when compiled with -DSINGLE_THREAD
|
2019-06-05 12:11:27 +01:00 |
|
Nuno Lopes
|
9b375150eb
|
remove remaining _NO_OMP_
|
2019-06-05 10:07:16 +01:00 |
|
Nuno Lopes
|
37882f5afa
|
fix race condition in cooperate
|
2019-06-05 09:31:45 +01:00 |
|
Nikolaj Bjorner
|
7f74382863
|
capture i by value
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-05 09:06:18 +01:00 |
|
Nikolaj Bjorner
|
27971e3f68
|
exception behavior in C++11 threads?
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-05 09:06:17 +01:00 |
|
Nikolaj Bjorner
|
9f3089b098
|
try with std::vector and ptr_vectors
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-05 09:06:17 +01:00 |
|
Nikolaj Bjorner
|
e4e60bff26
|
include thread in tactical
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-05 09:06:17 +01:00 |
|
Nikolaj Bjorner
|
f5511b4174
|
missing include
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-05 09:06:17 +01:00 |
|
Nikolaj Bjorner
|
1f84381c4c
|
pfor
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-05 09:06:17 +01:00 |
|
Nikolaj Bjorner
|
59330b3855
|
pfor
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-05 09:06:17 +01:00 |
|
Nikolaj Bjorner
|
9262908ebb
|
mux
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-05 09:06:17 +01:00 |
|
Nikolaj Bjorner
|
2788f72bbb
|
don't lose equalities over ite, #2317
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-04 20:32:24 -07:00 |
|
Nikolaj Bjorner
|
51b75a132c
|
signed char -> int, update mk_util to catch warnings on fptest, thanks to jfc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-02 17:22:36 -07:00 |
|
Nikolaj Bjorner
|
6fdef691e5
|
fix #2316
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-02 16:37:38 -07:00 |
|
Nikolaj Bjorner
|
1d46d5c870
|
use signed char per porting issue for ARM/64
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-02 15:53:32 -07:00 |
|
Nikolaj Bjorner
|
cccd37101e
|
fix #2314
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-01 20:34:58 -07:00 |
|
Bruce Mitchener
|
a12de12515
|
Use const& to reduce copies.
|
2019-06-02 09:58:32 +07:00 |
|
Nikolaj Bjorner
|
62de187d02
|
Merge pull request #2311 from waywardmonkeys/fix-reorder-warning
Fix -Wreorder warning.
|
2019-06-02 02:57:24 +02:00 |
|
Nikolaj Bjorner
|
3c3e5d7f7d
|
Merge pull request #2313 from waywardmonkeys/fix-cppapi-comment-typo
Fix C++ API comment typo.
|
2019-06-02 02:56:52 +02:00 |
|
Bruce Mitchener
|
17a0d75436
|
Fix C++ API comment typo.
|
2019-06-01 15:57:56 +07:00 |
|
Bruce Mitchener
|
960b8566f5
|
Fix some unused variable warnings.
|
2019-06-01 15:45:17 +07:00 |
|
Bruce Mitchener
|
759811b308
|
Fix -Wreorder warning.
|
2019-06-01 15:44:21 +07:00 |
|
Nikolaj Bjorner
|
01f6489892
|
fix #2310
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-31 16:22:49 -07:00 |
|
Nikolaj Bjorner
|
dd452e0ac1
|
eq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-31 15:29:27 -07:00 |
|
Nikolaj Bjorner
|
e79542cc68
|
fix #2309
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-31 07:46:11 -07:00 |
|
Nikolaj Bjorner
|
f1dee935d0
|
remove UNREACHABLE
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-30 17:07:00 -07:00 |
|
Nikolaj Bjorner
|
f11cb77c3d
|
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-30 16:15:55 -07:00 |
|
Nikolaj Bjorner
|
8893913c98
|
remove internal referenes to set_activity
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-30 16:06:05 -07:00 |
|
Nikolaj Bjorner
|
fc4c162e31
|
add clause proof module, small improvements to bapa
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-30 15:59:28 -07:00 |
|
Nikolaj Bjorner
|
f128398bf9
|
add clause proof module, small improvements to bapa
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-30 15:57:19 -07:00 |
|
Nikolaj Bjorner
|
48fc3d752e
|
add clause proof module, small improvements to bapa
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-30 15:49:19 -07:00 |
|
Nikolaj Bjorner
|
25c93410b1
|
add #2298 to regression/example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-29 07:24:42 -07:00 |
|
Nikolaj Bjorner
|
8f36868285
|
fix #2300
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-27 09:35:55 -07:00 |
|
Nikolaj Bjorner
|
f99384c6a3
|
fix nightly regression from solve-eqs context solver addition
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-27 04:17:43 -07:00 |
|
Nikolaj Bjorner
|
2d0ff7d68a
|
print literals more compactly
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-24 15:39:35 +02:00 |
|
Nikolaj Bjorner
|
8243139fb0
|
handle div 0 cases as it is uninterpreted #1683
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-24 07:00:56 +04:00 |
|
Nikolaj Bjorner
|
e49e5d7145
|
fix #2297
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-24 06:55:06 +04:00 |
|
Nikolaj Bjorner
|
faf4ba8309
|
add check for contravariance to fix #2256
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-22 18:32:57 +04:00 |
|
Nikolaj Bjorner
|
082a0f4df4
|
add get_lstring per #2286
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-22 18:32:57 +04:00 |
|
Nikolaj Bjorner
|
b2845d888e
|
add get_lstring per #2286
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-22 18:32:57 +04:00 |
|