mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity
11593 commits 23 branches 48 tags 157 MiB
Commit graph

11593 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
41ca956012 expose import model converter over Python, document it, add partial order axioms for lex, disable linear order axioms, prepare ground for re-adding clauses from reconstruction stack 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-18 13:45:13 -07:00
Nikolaj Bjorner
7ed5ca05e3 fix #2408 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-18 08:37:00 -07:00
Nikolaj Bjorner
d07f2d45e7 fix #2409 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-18 08:33:58 -07:00
Nikolaj Bjorner
1fca76b0a1 relax restriction on infinitesimal for rdl, #2410 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-18 08:26:23 -07:00
Nikolaj Bjorner
5820b16800 mark assumption literals to be skolem to hide them from models #2406 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-18 08:25:42 -07:00
Nikolaj Bjorner
4b6a7371dd insert fresh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-18 06:31:47 -07:00
Nikolaj Bjorner
fb124d6e93
Merge pull request #2393 from Nils-Becker/master 
Fix Incorrect Logging of Newly Introduced Terms During Rewrite
 2019-07-14 09:25:06 -04:00
Nikolaj Bjorner
4deb9d2af2 use array interpretations whenever possible for #2378. Also strengthen equality test for lambda 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-14 09:23:29 -04:00
Nikolaj Bjorner
3ca32efd18 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-13 16:22:09 -04:00
Nikolaj Bjorner
2d4e9a0f67 update managed APIs for lambda-based array models #2400 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-13 16:20:36 -04:00
Nikolaj Bjorner
659be6940b fix #2395 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-12 18:01:26 -04:00
Nikolaj Bjorner
26c1c744aa fix #2396 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-12 17:36:30 -04:00
Nikolaj Bjorner
0bca2aabff remove invocation of debugger 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-12 17:07:44 -04:00
Nikolaj Bjorner
559af09b07 fix index cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-12 19:01:39 +01:00
Nikolaj Bjorner
84990ffa27 fixing #2378 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-12 14:21:22 +01:00
Nikolaj Bjorner
be72accaf5 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-12 12:37:46 +01:00
Nikolaj Bjorner
1538b31dd9 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-12 12:37:24 +01:00
Nikolaj Bjorner
d861b91289 augment axiomatization for substr to fix #2366 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-12 11:13:05 +01:00
Nikolaj Bjorner
79e4b84507 augment axiomatization for substr to fix #2366 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-12 11:12:01 +01:00
Nikolaj Bjorner
1ba6d16c61 augment axiomatization for substr to fix #2366 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-12 08:38:33 +01:00
nilsbecker
308647efd9 Merge branch 'master' of https://github.com/Z3Prover/z3 2019-07-11 17:22:10 +02:00
nilsbecker
335072eda2 extract logging into separate function 2019-07-11 17:22:03 +02:00
Nikolaj Bjorner
cfb4d289b8 fix #2325 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-11 10:34:35 +01:00
Nikolaj Bjorner
c7fb1e4c9f fix spelling of target folder 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-11 09:56:08 +01:00
Nikolaj Bjorner
9474833c98 fix #2391 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-11 09:26:22 +01:00
Nikolaj Bjorner
adb91ae93c compile 0 case regardless of numerical value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-11 09:07:18 +01:00
Nikolaj Bjorner
77df8ebd12 try to copy artifacts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-10 16:23:02 +01:00
Nikolaj Bjorner
8d9a631c5d try to copy artifacts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-10 16:21:14 +01:00
Nils Becker
1d859a98e5 updating comment 2019-07-10 17:12:08 +02:00
Nils Becker
7a48524213 count subterm references correctly 2019-07-10 17:09:21 +02:00
Nils Becker
b226f3a77c cleaning up includes 2019-07-10 16:43:48 +02:00
Nils Becker
035101f399 Merge branch 'master' of https://github.com/Z3Prover/z3 into HEAD 2019-07-10 16:18:00 +02:00
Nils Becker
23d01f5974 fixing rewrite logging (https://bitbucket.org/viperproject/axiom-profiler/issues/13/version-486-of-z3-not-compatible-with) 2019-07-10 16:17:30 +02:00
Nikolaj Bjorner
09328d5bec remove unknown option /RELEASE in python build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-10 14:52:41 +01:00
Nikolaj Bjorner
ee94f8f5ce update release script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-10 13:52:41 +01:00
Nikolaj Bjorner
5de35d46eb fix #2390 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-10 08:55:00 +01:00
Nikolaj Bjorner
a13ac6a759
Merge pull request #2389 from agurfinkel/issue_2357 
Uses non-flattening rewriter in profos
 2019-07-10 08:54:44 +01:00
Arie Gurfinkel
7cb956a0e2 Uses non-flattening rewriter in profos 2019-07-09 13:30:11 -04:00
Nikolaj Bjorner
88aa689a70 fix #2387, add ite-hoist rewriting, allow assumptions to be compound expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-09 07:40:29 +01:00
Nikolaj Bjorner
cd93cdd819 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-09 07:40:29 +01:00
Nuno Lopes
6bbe8e2619 add some static 2019-07-07 15:30:32 +01:00
Nikolaj Bjorner
6e63734882
Merge pull request #2368 from waywardmonkeys/fix-typo 
Python: Fix doc comment typo.
 2019-07-05 14:38:32 +07:00
Nikolaj Bjorner
164039a47c
Merge pull request #2383 from mcfi/patch-2 
Pass /RELEASE to MSVC linker
 2019-07-05 14:37:30 +07:00
Nikolaj Bjorner
dd253cdd47
Merge pull request #2382 from mcfi/patch-1 
Remove unreferenced formal parameter name
 2019-07-05 08:33:23 +07:00
Ben Niu
962d0dda78
Pass /RELEASE to MSVC linker 
Without /RELEASE passed to MSVC linker, the checksum field in exe/dll is not calculated. When you load the exe/dll in windbg (e.g., windbg -z libz3.dll), a warning "Unable to verify checksum" will show. With /RELEASE passed to linker, the warning will be gone.
 2019-07-04 08:08:32 -07:00
Ben Niu
f8a9f6cce0
Remove unreferenced formal parameter name 
MSVC reports warning C4100 when compiling z3++.h, because of unreferenced formal parameter.
 2019-07-04 08:01:40 -07:00
Nikolaj Bjorner
6d244ed2aa internalize reflect 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-04 07:33:37 +07:00
Nikolaj Bjorner
b86432e2a3 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-04 07:26:50 +07:00
Nikolaj Bjorner
c744b19bce resort to only supporting ground non-linear division for nra_tactic/nra_probe #2372 #2376 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-04 07:08:47 +07:00
Nikolaj Bjorner
8e2ad4e461 #2379 and #2380 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-04 07:08:47 +07:00