Nikolaj Bjorner
|
a22fb8a96e
|
revert unit propagation of equality literals
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-18 23:11:03 -08:00 |
|
Nikolaj Bjorner
|
27584d68db
|
more rewrite rules
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-18 22:14:53 -08:00 |
|
Nikolaj Bjorner
|
b2eb248bad
|
fixes, fix #5034
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-18 16:47:44 -08:00 |
|
Nikolaj Bjorner
|
180015a529
|
fix #5035
|
2021-02-18 16:47:36 -08:00 |
|
Murphy Berzish
|
27db97c269
|
Z3str3: add str.to_code and str.from_code (#5015)
|
2021-02-18 16:51:34 -06:00 |
|
Nikolaj Bjorner
|
ca9fcbd1df
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-18 13:46:59 -08:00 |
|
Nikolaj Bjorner
|
00dab30ea0
|
remove binary_function
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-18 13:18:58 -08:00 |
|
Nikolaj Bjorner
|
9ae3339c33
|
fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-18 12:33:17 -08:00 |
|
Nuno Lopes
|
c9d6dccc12
|
travis fixes
|
2021-02-18 19:52:30 +00:00 |
|
Nuno Lopes
|
14de590566
|
fix MSVC build
|
2021-02-18 19:05:20 +00:00 |
|
Nuno Lopes
|
1105f4aea8
|
update travis to ubuntu 18.04
just 1 LTS old
|
2021-02-18 18:46:30 +00:00 |
|
Nuno Lopes
|
d396d46bd1
|
let's test if all the buildbots are happy with C++17
it's stil a bit too early for C++20
|
2021-02-18 18:13:10 +00:00 |
|
Nikolaj Bjorner
|
e63dc7efc2
|
more rewrite rules
|
2021-02-17 17:32:00 -08:00 |
|
Nuno Lopes
|
bcad4d9435
|
revert my mess with the ast hashtable
will share results form the experiments later
|
2021-02-17 14:29:07 +00:00 |
|
Nikolaj Bjorner
|
4f9117a921
|
Move seq axioms to theory independent module
|
2021-02-16 05:13:52 -08:00 |
|
Nikolaj Bjorner
|
823830181b
|
butterfly effect with relevancy marking
bail out of infinite instantiation loop
|
2021-02-15 16:37:23 -08:00 |
|
Nikolaj Bjorner
|
a6dce246f6
|
fix #5031
|
2021-02-15 14:36:01 -08:00 |
|
Nikolaj Bjorner
|
96e7b811f9
|
fix #5029
|
2021-02-15 14:17:05 -08:00 |
|
Nikolaj Bjorner
|
c387863da1
|
fix #5032, reset substitution during fold transformation
|
2021-02-15 14:14:25 -08:00 |
|
Nikolaj Bjorner
|
6bd02e122b
|
parse according to http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-15 09:32:31 -08:00 |
|
Nikolaj Bjorner
|
1da7522893
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-14 17:47:19 -08:00 |
|
Nikolaj Bjorner
|
70b4822571
|
patch seq theory using purification to avoid unsoundness caused by interaction with canonization and rewriting
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-02-14 17:41:06 -08:00 |
|
Nuno Lopes
|
2db2767e7a
|
remove unused method
in preparation for a bigger storm :)
|
2021-02-14 23:31:24 +00:00 |
|
Nikolaj Bjorner
|
eac69c5504
|
incorrect axiomatization
Fixes repro in https://github.com/Z3Prover/z3/issues/4866#issuecomment-778706682
|
2021-02-14 15:29:10 -08:00 |
|
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 |
|