mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
12881 commits 49 branches 53 tags 182 MiB
Commit graph

12881 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
4c0db00a7b fix push/pop bug for ite-elimination, thanks to Nao Hirokawa for reporting it 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-30 08:31:37 -03:00
Nikolaj Bjorner
de43e05102 fix overflow bug exposed by #2476 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-29 22:34:04 -03:00
Nikolaj Bjorner
a8bfab3273 add model.inline_def option to make #2517 happy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-29 12:08:09 -03:00
Nikolaj Bjorner
35fa24a82a initialize best model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-28 12:31:13 -03:00
Nikolaj Bjorner
20dc59e02d fix #2523 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-28 12:28:33 -03:00
Nikolaj Bjorner
2e6908bd9e fix #2509, fix issue with model inheritance exposed by #2483 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-27 10:48:22 -03:00
Nikolaj Bjorner
271cd2ac6b disable expensive model validation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-26 07:26:12 -03:00
Nikolaj Bjorner
f048cb27ba revert the revert 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-25 16:05:57 -03:00
Nikolaj Bjorner
75a40d8f8e reorder fields, rename overload name clash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-25 16:01:39 -03:00
Nikolaj Bjorner
64f4c9794d fix regressions during string fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-25 10:00:26 +01:00
Nikolaj Bjorner
0d9cd7bc2b addressing misc. string bugs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-24 15:40:15 +01:00
Nikolaj Bjorner
a337a51374 fixes for #2513 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-23 23:29:24 +03:00
Nikolaj Bjorner
de69b01e92 Lev's fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-23 23:29:24 +03:00
Nikolaj Bjorner
f90db2ba1c add back compression to ensure local functions are inlined #2517 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-23 21:35:45 +03:00
Nikolaj Bjorner
c15764e06d remove verbose=0 instances #2507 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-21 21:40:51 +08:00
Nikolaj Bjorner
ffc696e634 exclude built-in functions from model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-21 12:05:52 +08:00
Nikolaj Bjorner
eea041383d fix #2502 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-21 11:11:22 +08:00
Nikolaj Bjorner
e08abb3213 fix #2504 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-21 10:06:43 +08:00
Christoph M. Wintersteiger
2f60bcbfcb
Clean up NaN return values in Z3_get_numeral_double 2019-08-19 14:43:39 +01:00
Christoph M. Wintersteiger
423fb73d34
Fix for fp.rem. Pertains to #2381. 2019-08-19 13:13:01 +01:00
Christoph M. Wintersteiger
f22d6e399d
Fix floats in Z3_get_numeral_*string. 2019-08-19 13:10:43 +01:00
Christoph M. Wintersteiger
79cd1f0edc
Fixed Z3_get_numeral_double. Fixes #2501. 2019-08-19 12:37:02 +01:00
Bruce Mitchener
258b798a6b test-z3: Improve help output. Provide help when no args. 2019-08-16 03:20:57 -07:00
Bruce Mitchener
f02170feb4 Clean up whitespace. 2019-08-16 03:20:57 -07:00
Nikolaj Bjorner
fcc7bd35e5 fix #2489 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-15 21:04:04 -07:00
Nikolaj Bjorner
3074e2b80c fix #2487 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-15 10:24:28 -07:00
Bruce Mitchener
d64dc939b2 Add note about minimized unsat cores to C API docs. 2019-08-15 10:20:41 -07:00
Bruce Mitchener
9949f16525 Fix release note typos. 2019-08-15 10:20:03 -07:00
Bruce Mitchener
e2122c0d3d Fix whitespace issues in *.pyg. 2019-08-15 10:19:33 -07:00
Nikolaj Bjorner
0734c5f3f3 fix is-array-sort test again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-15 10:18:50 -07:00
Christoph M. Wintersteiger
892aa12660
Fix for fp.rem. Fixes #2381. 2019-08-15 16:44:55 +01:00
Bruce Mitchener
0edd587e5a Fix typos in examples. 2019-08-14 22:00:50 -07:00
Audrey Dutcher
ec5b148ecc Add python packaging build and deployment with Azure 2019-08-14 22:00:21 -07:00
Nikolaj Bjorner
eec550e645 fix python build break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-14 21:59:53 -07:00
Nikolaj Bjorner
2b2f016f96 python for accessing lambda, switch to theory branching for QF_LRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-14 15:44:34 -07:00
Nikolaj Bjorner
520ea65f32 move towards theory phase selection, implement getitem on lambda 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-14 15:44:33 -07:00
Bruce Mitchener
0eafeb9342 Fix confusing tabs mixed in with spaces in C examples. 2019-08-13 09:26:44 -07:00
Phillip Schanely
0093157bb9 Handle dynamic sort of Nth()'s return value in the Python API 2019-08-13 09:26:10 -07:00
Bruce Mitchener
e89bb37156 More see also content in C API docs. 2019-08-13 09:25:27 -07:00
Everett Maus
73083977e2 Trying a different clang version that should be installed 2019-08-12 17:31:57 -07:00
Everett Maus
8e3f5b0c1d Add MSAN_SYMBOLIZER_PATH to the environment to get symbolization 2019-08-12 15:56:50 -07:00
Arie Gurfinkel
375c0ff9a9 Implement get_proof() in bmc and spacer engines 2019-08-12 10:29:01 -07:00
Nikolaj Bjorner
876cfb4dc9 optimization of phase 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-12 09:50:31 -07:00
Nikolaj Bjorner
75962173ff fix #2481 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-12 09:38:45 -07:00
Nikolaj Bjorner
9fa9aa09ff fix #2468, adding assignment phase heuristic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-10 15:25:05 -07:00
Nikolaj Bjorner
42e21458ba fix #2479 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-09 17:06:05 -07:00
Nikolaj Bjorner
ce84e0f240 remove strategic solver header file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-09 15:56:04 -07:00
Nikolaj Bjorner
fc41a61b6e expose strategic solver factory prototype at level of solver module 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-09 15:52:12 -07:00
Nikolaj Bjorner
1ae0a98132 fix #2466 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-09 13:37:22 -07:00
Arie Gurfinkel
52acbf1f14 bug in qe_lite 2019-08-09 13:31:49 -07:00