diff --git a/submissions/z3_base.json b/submissions/z3_base.json new file mode 100644 index 00000000..28a59e80 --- /dev/null +++ b/submissions/z3_base.json @@ -0,0 +1,30 @@ +{ + "name": "Z3-4.15.0", + "contributors": [ + "Nikolaj Bjørner et al." + ], + "contacts": ["Nikolaj Bjørner "], + "archive": { + "url": "https://zenodo.org/records/15687848/files/z3.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", + "Bitvec", + "QF_Bitvec", + "QF_LinearIntArith", + "QF_LinearRealArith", + "QF_NonLinearIntArith", + "QF_NonLinearRealArith", + "QF_Strings" + ] + } + ] +} \ No newline at end of file diff --git a/submissions/z3alpha.json b/submissions/z3alpha.json new file mode 100644 index 00000000..97a19e9f --- /dev/null +++ b/submissions/z3alpha.json @@ -0,0 +1,33 @@ +{ + "name": "Z3-alpha", + "contributors": [ + "John Lu", + "Paul Sarnighausen-Cahn", + "Jiahao Chen", + "Florin Manea", + "Vijay Ganesh" + ], + "contacts": ["John Lu "], + "archive": { + "url": "https://zenodo.org/records/15765918/files/submission25.zip?download=1" + }, + "website": "https://github.com/JohnLyu2/z3alpha", + "system_description": "https://drive.google.com/uc?export=download&id=17n4WbrukfKz7CxdVBXtSQjU_EYmwo1ZR", + "solver_type": "derived", + "command": ["./z3alpha.py"], + "seed": "33", + "participations": [ + { + "tracks": ["SingleQuery"], + "divisions": [ + "Arith", + "QF_Bitvec", + "QF_LinearIntArith", + "QF_LinearRealArith", + "QF_NonLinearIntArith", + "QF_NonLinearRealArith", + "QF_Strings" + ] + } + ] +} \ No newline at end of file