SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2021

Rules
Benchmarks
Tools
Specs
Parallel & Cloud Tracks
Participants

iProver

Competing yes
Single Query Track LIA, LRA, NIA, NRA, UF, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA
Incremental Track
Unsat Core Track
Model Validation Track
Cloud Track
Parallel Track
Preliminary ID 33293
Final ID 33459
Seed 12281
System Description iProver-v3.5 (SMT-COMP 2021)
Variant of Submission ID
Derived from Solver
Wrapped Solvers Vampire is used for clausification and theory axiomatisations; Z3 and MiniSAT for ground reasoning
Website http://www.cs.man.ac.uk/~korovink/iprover/
Team Members Konstantin Korovin, Andre Duarte, Edvard K Holden
Contact konstantin.korovin@manchester.ac.uk