diff --git a/submissions/z3gex-base.json b/submissions/z3gex-base.json new file mode 100644 index 000000000..42cdc9839 --- /dev/null +++ b/submissions/z3gex-base.json @@ -0,0 +1,37 @@ +{ + "name": "Z3-GEX-base", + "contributors": [ + "Nikolaj Bjørner et al." + ], + "contacts": [ + "Nikolaj Bjørner " + ], + "archive": { + "url": "https://zenodo.org/records/20615910/files/Z3_base.zip?download=1" + }, + "website": "https://github.com/Z3Prover/z3", + "system_description": "https://link.springer.com/content/pdf/10.1007/978-3-540-78800-3_24.pdf", + "solver_type": "Standalone", + "command": [ + "./z3" + ], + "seed": "33", + "participations": [ + { + "tracks": [ + "SingleQuery" + ], + "divisions": [ + "Arith", + "QF_Bitvec", + "QF_LinearIntArith", + "QF_LinearRealArith", + "QF_NonLinearIntArith", + "QF_NonLinearRealArith", + "QF_Strings" + ] + } + ], + "competitive": false, + "final": true +} \ No newline at end of file diff --git a/submissions/z3gex.json b/submissions/z3gex.json new file mode 100644 index 000000000..5f278b73a --- /dev/null +++ b/submissions/z3gex.json @@ -0,0 +1,39 @@ +{ + "name": "Z3-GEX", + "contributors": [ + "Shuming Shi", + "Wenbo Wei", + "Zhengfeng Yang", + "Jianlin Wang" + ], + "contacts": [ + "Wenbo Wei " + ], + "archive": { + "url": "https://zenodo.org/records/20642639/files/Z3_GEX.zip?download=1" + }, + "website": "https://github.com/moyvbai/smt-comp2026", + "system_description": "https://github.com/moyvbai/smt-comp2026/blob/main/SMT.pdf", + "command": [ + "z3gex" + ], + "solver_type": "derived", + "seed": "42", + "participations": [ + { + "tracks": [ + "SingleQuery" + ], + "divisions": [ + "Arith", + "QF_Bitvec", + "QF_LinearIntArith", + "QF_LinearRealArith", + "QF_NonLinearIntArith", + "QF_NonLinearRealArith", + "QF_Strings" + ] + } + ], + "final": true +} \ No newline at end of file