|
1 | 1 | { |
2 | 2 | "name": "Z3-Owl", |
3 | 3 | "contributors": [ |
4 | | - "First Smith", |
5 | | - { "name": "Second Baker", "website": "http://baker.com/" } |
| 4 | + "Hanrui Zuo", "Peisen Yao" |
6 | 5 | ], |
7 | | - "contacts": [ "contact name <[email protected]>"], |
| 6 | + "contacts": [ "Peisen Yao <[email protected]>"], |
8 | 7 | "archive": { |
9 | | - "url": "http://example.com/solver.tar.gz", |
10 | | - "h": { "sha256": "012345" } |
| 8 | + "url": "https://drive.usercontent.google.com/download?id=1NvC4K6oGYN6DP40wUh-oL6JiIBvfKG64&export=download", |
| 9 | + "h": { "sha256": "14481e149fccc581a67691424294113ded5eae104b74615efbd77f6c1fe968fb" } |
11 | 10 | }, |
12 | | - "website": "http://example.com/", |
| 11 | + "website": "https://rainoftime.github.io/html/owl.html", |
13 | 12 | "system_description": "http://example.com/system.pdf", |
14 | | - "command": ["relative_cmd", "default_command_line"], |
15 | | - "solver_type": "Standalone", |
16 | | - "seed": "42", |
| 13 | + "command": ["Z3-Owl"], |
| 14 | + "solver_type": "derived", |
17 | 15 | "participations": [ |
18 | | - { "tracks": ["SingleQuery"], "divisions": ["Equality"] }, |
19 | 16 | { |
20 | 17 | "tracks": ["SingleQuery"], |
21 | | - "logics": "QF_.*LRA.*", |
22 | | - "command": ["relative_cmd", "other_option"] |
23 | | - }, |
24 | | - { |
25 | | - "tracks": ["SingleQuery"], |
26 | | - "logics": ["LIA"], |
27 | | - "archive": { "url": "http://example.com/solver_lia.tar.gz" }, |
28 | | - "command": ["relative_cmd", "--super-lia"] |
| 18 | + "logics": [ |
| 19 | + "QF_BV", |
| 20 | + "QF_UFBV", |
| 21 | + "QF_ABV", |
| 22 | + "QF_AUFBV", |
| 23 | + "QF_FP", |
| 24 | + "QF_BVFP" |
| 25 | + ] |
29 | 26 | } |
30 | 27 | ] |
31 | 28 | } |
0 commit comments