Nikolaj Bjorner
|
45af1bd243
|
fix build, move seq_skolem
|
2021-02-14 14:40:29 -08:00 |
|
Nikolaj Bjorner
|
083d09aa81
|
fix #5016
|
2021-02-14 13:52:10 -08:00 |
|
Nikolaj Bjorner
|
04a1d4245c
|
fix #4801
|
2021-02-12 20:20:00 -08:00 |
|
Nikolaj Bjorner
|
83f4a006c6
|
wreckfun
|
2021-02-12 19:46:47 -08:00 |
|
Nikolaj Bjorner
|
612cc5cfba
|
fix #5014
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-12 16:01:33 -08:00 |
|
Nikolaj Bjorner
|
85f0084e9c
|
set options and change VS for nightly
|
2021-02-12 13:41:30 -08:00 |
|
Nikolaj Bjorner
|
4991c6c2c6
|
fix #5002
Avoid code path that uses qe_tactic as it isn't protected against parameter abuse
|
2021-02-12 13:20:51 -08:00 |
|
Nikolaj Bjorner
|
80d297dca2
|
Try to move using windows latest instead of VS2017
|
2021-02-12 12:45:21 -08:00 |
|
Nikolaj Bjorner
|
998cf4c726
|
fix #5020
comparison for strict neighbor relation seemed reversed.
Alas, this could introduce additional regressions
|
2021-02-12 12:24:27 -08:00 |
|
Nikolaj Bjorner
|
c808f74591
|
fix multiplier base for #5022
add also some C++ API shorthands for retrieving numerals
|
2021-02-12 11:53:40 -08:00 |
|
Nikolaj Bjorner
|
d0c96abe30
|
log classificaiton
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-11 14:44:05 -08:00 |
|
Nikolaj Bjorner
|
1d12b72bbc
|
log classificaiton
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-11 14:43:05 -08:00 |
|
Nikolaj Bjorner
|
25f53c0467
|
deal with warnings reported in https://launchpadlibrarian.net/522361319/buildlog_ubuntu-groovy-s390x.z3_4.8.10-1ubuntu4ppa1_BUILDING.txt.gz
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-11 13:49:47 -08:00 |
|
Nikolaj Bjorner
|
2e648e2f02
|
glibc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-11 13:19:23 -08:00 |
|
Nikolaj Bjorner
|
98eae28fca
|
try to update setup.py to libc naming
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-11 11:52:05 -08:00 |
|
Nikolaj Bjorner
|
b6294ab235
|
is glibc the new centos?
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-11 11:17:33 -08:00 |
|
Nikolaj Bjorner
|
c03bd5e1c8
|
is glibc the new centos?
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-11 11:17:04 -08:00 |
|
Nikolaj Bjorner
|
5d46ac0aca
|
is glibc the new centos?
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-11 11:14:39 -08:00 |
|
Nikolaj Bjorner
|
b7d1d03b08
|
try revert to u18 for centos zip
|
2021-02-11 10:36:48 -08:00 |
|
Nikolaj Bjorner
|
2301fce65e
|
it helps to spell
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-11 09:44:03 -08:00 |
|
Nikolaj Bjorner
|
9883a0b983
|
downgrade to Ubuntu 18 for ocaml doc build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-11 09:43:22 -08:00 |
|
Nikolaj Bjorner
|
9cdb875ba2
|
remove use of deprecated linux_distribution
|
2021-02-11 09:40:23 -08:00 |
|
Nikolaj Bjorner
|
53e98a27db
|
adding stubs
|
2021-02-11 09:36:47 -08:00 |
|
Don Syme
|
504b6559ab
|
[WIP] Suggestion: build .NET package for both x86 and x64 and rename (#5021)
* build package for x86
* build package for x86
* build package for x86
Co-authored-by: Don Syme <donsyme@fastmail.com>
|
2021-02-11 09:29:32 -08:00 |
|
Nikolaj Bjorner
|
4c3c15c015
|
Propagate reason for undef as exception to improve error reporting in scenarios such as #5009
|
2021-02-09 16:58:01 -08:00 |
|
Nikolaj Bjorner
|
5c04b9eee2
|
fix #5012
teething stage for from/to code axiomatization
|
2021-02-09 16:38:03 -08:00 |
|
Nikolaj Bjorner
|
692f159af8
|
try without format
|
2021-02-09 12:49:55 -08:00 |
|
Nikolaj Bjorner
|
e722589810
|
address some of the ugliness pointed out by abandoned pull request #5008
|
2021-02-09 11:23:16 -08:00 |
|
Nikolaj Bjorner
|
8b5094fe73
|
provide additional diagnostics for #5009
|
2021-02-09 10:14:38 -08:00 |
|
Nikolaj Bjorner
|
8ca2de41db
|
turn on from/to code handling #5007 samples
|
2021-02-09 10:00:08 -08:00 |
|
Nikolaj Bjorner
|
cbb570051c
|
#5007 - wrong recognizer function definitions
|
2021-02-09 09:54:24 -08:00 |
|
Nikolaj Bjorner
|
55cb12e233
|
build fix
|
2021-02-08 16:53:30 -08:00 |
|
Nikolaj Bjorner
|
a152bb1e80
|
remove template Context dependency in every trail object
|
2021-02-08 15:41:57 -08:00 |
|
Nikolaj Bjorner
|
df0a449f70
|
fix some build warnings exposed in #5005
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-08 10:58:42 -08:00 |
|
Nikolaj Bjorner
|
b56372fe76
|
fix some build warnings exposed in #5005
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-08 10:57:50 -08:00 |
|
Nikolaj Bjorner
|
8fffc03263
|
remove bv dependencies
|
2021-02-08 10:57:50 -08:00 |
|
Nikolaj Bjorner
|
0f29fff836
|
remove bit-vector dependencies in seq theory
|
2021-02-08 10:57:50 -08:00 |
|
Nikolaj Bjorner
|
43d1ef2fee
|
iterable is a Python 3 thingy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-07 18:22:57 -08:00 |
|
Nuno Lopes
|
52e67b0d3e
|
switch expr_safe_replace to std::unordered_map (#5003)
* switch expr_safe_replace to std::unordered_map
* further tweaks to expr_safe_replace for an overall speedup of 1.x in Z3_substitute
|
2021-02-07 18:20:48 -08:00 |
|
Nuno Lopes
|
615cafe39b
|
remove unneded pragma once
|
2021-02-07 12:54:17 +00:00 |
|
Nuno Lopes
|
682b947ad3
|
the documentation of Z3_model_get_func_interp() says it returns NULL if there's no interpretation
so let's honour that instead of throwing an exception
|
2021-02-07 12:46:36 +00:00 |
|
Nuno Lopes
|
e1572096ca
|
delete some dead code
|
2021-02-07 12:14:52 +00:00 |
|
Julius Marozas
|
01d5f3259c
|
Fix show parameter in prove, solve, and solve_using (#5001)
* Fix show parameter in prove function
* Fix show in solve & solve_using
* Use Python 2 compatible syntax
* Add default value for show
|
2021-02-06 16:42:15 -08:00 |
|
Nikolaj Bjorner
|
e856cfc458
|
coercions
|
2021-02-06 10:35:28 -08:00 |
|
Nikolaj Bjorner
|
16448104eb
|
add new model event handler for incremental optimization
|
2021-02-05 17:11:04 -08:00 |
|
Nikolaj Bjorner
|
2c472aaa10
|
#4999
use typing Iterable
|
2021-02-05 12:09:24 -08:00 |
|
Nikolaj Bjorner
|
a582014854
|
#4999
|
2021-02-05 12:01:30 -08:00 |
|
Nikolaj Bjorner
|
0a9ee6c640
|
build break
|
2021-02-04 16:58:32 -08:00 |
|
Malte Mues
|
5d8d42b1fa
|
Update the mkConstant parameter type (#4996)
|
2021-02-04 16:17:49 -08:00 |
|
Nikolaj Bjorner
|
0ec567fe15
|
integrate v2 of lns
|
2021-02-04 15:47:40 -08:00 |
|