mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
15146 commits 49 branches 53 tags 182 MiB
Commit graph

15146 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
64ba2a9fc9 fix gc of pb constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-19 03:38:00 -08:00
Nikolaj Bjorner
01418a06a3 better staging of mbi based on generation 2021-01-18 16:55:58 -08:00
Nikolaj Bjorner
990aecceb7 change gc strategy for user-push/pop 2021-01-18 16:55:29 -08:00
Nikolaj Bjorner
b87405cc92 tune user-pop 2021-01-18 16:51:34 -08:00
Nikolaj Bjorner
3ed490d4ed tune backtracking 2021-01-18 16:51:01 -08:00
Nikolaj Bjorner
91c54f6c39 na 2021-01-12 14:03:55 -08:00
Nikolaj Bjorner
8abb644378 add xml file to the mix #4578 2021-01-12 00:23:02 -08:00
Nikolaj Bjorner
d1dab327cd fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-11 23:51:40 -08:00
Nikolaj Bjorner
fc3a642876 fix #4948 2021-01-11 19:26:16 -08:00
Nikolaj Bjorner
0aac7e54a9 fix #4942 
Patching model update. Could use a more thorough revision.
 2021-01-11 15:48:49 -08:00
Nikolaj Bjorner
0e429cab33 enable new core for incremental mode 2021-01-11 14:55:31 -08:00
Nikolaj Bjorner
2ead209d40 indentation and updated links to default landing pages 2021-01-11 13:21:52 -08:00
Nikolaj Bjorner
bcbda45298 updates to doc 2021-01-11 13:03:55 -08:00
Nikolaj Bjorner
396bfa05f3 fix grouping error 2021-01-11 12:25:53 -08:00
Nikolaj Bjorner
223bffd035 fix #4920 2021-01-09 02:02:50 -08:00
Nikolaj Bjorner
1a71dfac6f play nicebox #4918 2021-01-09 01:39:29 -08:00
Nikolaj Bjorner
96ab9edbfd fix #4923 2021-01-09 01:21:50 -08:00
Nikolaj Bjorner
ffd57bef24 #4923 - eq2bv 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-08 16:38:07 -08:00
Nikolaj Bjorner
690bc51b7f fix #4927 2021-01-08 15:40:15 -08:00
Nikolaj Bjorner
bb56443e71 more #4932 2021-01-08 15:24:12 -08:00
Nikolaj Bjorner
43eb862374 fix #4932 2021-01-08 12:50:36 -08:00
Nikolaj Bjorner
3d39f37e63 fix #4930 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-08 12:15:02 -08:00
Nikolaj Bjorner
e902e1ef13 fix #4931 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-08 12:02:53 -08:00
Nikolaj Bjorner
c36355c1e5 fix #4933 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-08 10:57:55 -08:00
Nikolaj Bjorner
0173359a50 debugging/testing mbi 2021-01-07 17:32:05 -08:00
Nikolaj Bjorner
4ca6d6951f use updated C++ features 2021-01-07 17:32:05 -08:00
Nikolaj Bjorner
ac7d07ca58 fix #4937 2021-01-07 17:32:05 -08:00
Nikolaj Bjorner
60ef60dff8 euf solver updates 2021-01-07 17:32:04 -08:00
Nikolaj Bjorner
7bf691e1f9 fix bug in tracking qhead 2021-01-07 17:32:04 -08:00
Nuno Lopes
4db41c02cc remove some dead code from fpa2bv converter 2021-01-04 17:06:35 +00:00
Nikolaj Bjorner
5da71dc847 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-30 16:10:11 -08:00
Nikolaj Bjorner
523578e3f6 working on new solver core 2020-12-30 14:38:41 -08:00
Nikolaj Bjorner
f519c58ace Add groovy R.U.Stan option to retrieve models even when they don't exist #4924 
Usage:
z3 4924.smt2 smt.candidate_models=true
 2020-12-30 14:38:41 -08:00
Nuno Lopes
799de71a9f
limit recursion depth of push_not() to 8 (#4917) 2020-12-28 19:55:43 -08:00
Nikolaj Bjorner
374ae52d70 testing mbi 2020-12-26 13:49:59 -08:00
Nikita Leshenko
d8eba2d72f
scripts/update_api: Replace Z3_LIBRARY_DIRS with Z3_LIB_DIRS (#4915) 
The error message that is printed when libz3.so can't be loaded contains
incorrect instruction to set `Z3_LIBRARY_DIRS` builtin. The correct variable
name is `Z3_LIB_DIRS`.

Signed-off-by: Nikita Leshenko <nikita@leshenko.net>
 2020-12-26 12:27:10 -08:00
Nikolaj Bjorner
372e5ca569 fixes in new solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-25 11:19:31 -08:00
Nikolaj Bjorner
21c626e3ee fix bound miss-computation, include sporadic nra check for #4913 2020-12-24 03:22:43 -08:00
Nikolaj Bjorner
8546cf97d7 on #4702 
Add weighting function to cycle more fairly through nla solvers.
Handles anomaly from https://github.com/Z3Prover/z3/files/5361721/pero.txt
 2020-12-24 03:07:25 -08:00
Nikolaj Bjorner
2679ae517b fix #4912 2020-12-23 15:04:25 -08:00
Nikolaj Bjorner
6284f6fb03 Update nightly.yaml for Azure Pipelines 2020-12-22 14:45:15 -08:00
Nikolaj Bjorner
9d22cf4d4f add signing to nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-22 13:13:04 -08:00
Nikolaj Bjorner
1c3b768ed0 update ubuntu version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-22 12:38:05 -08:00
Nikolaj Bjorner
0ed33af279 Update nightly.yaml for Azure Pipelines 2020-12-22 11:52:09 -08:00
Nikolaj Bjorner
8692fcdf3b Update nightly.yaml for Azure Pipelines 2020-12-22 10:47:33 -08:00
Nikolaj Bjorner
d72f6c80df Update nightly.yaml for Azure Pipelines 2020-12-22 09:58:03 -08:00
Nikolaj Bjorner
010d578e8f sym file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-21 18:08:23 -08:00
Nikolaj Bjorner
021bd8a994 sym file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-21 17:08:38 -08:00
Nikolaj Bjorner
f26662d079 na 2020-12-21 16:18:07 -08:00
Nikolaj Bjorner
3576b66e32 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-21 15:46:42 -08:00