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