CVC4 at SMT-COMP 2020

---

SMT-COMP 2020

Competing Version:  GitHub Branch smtcomp2020
System Description:  CVC4 at SMT-COMP 2020

Tracks Entered

---

• Single Query Track
  Divisions:  all divisions (68)
  Competing Binary:  StarExec Binary
• Incremental Track
  Divisions:  all divisions (28)
  Competing Binary:  StarExec Binary
• Unsat Core Track
  Divisions:  all divisions (41)
  Competing Binary:  StarExec Binary
• Model Validation Track
  Divisions:  all divisions (6)
  Competing Binary:  StarExec Binary

Track Awards

---

Single Query Track

• 1^st place in division ABVFP
• 1^st place in division ABVFPLRA
• 1^st place in division ALIA (unsat)
• 1^st place in division AUFBVDTLIA
• 1^st place in division AUFDTLIA
• 1^st place in division AUFDTLIRA
• 1^st place in division AUFDTNIRA (24s)
• 1^st place in division AUFFPDTLIRA
• 1^st place in division AUFLIA (sat)
• 1^st place in division AUFLIRA (sequential)
• 1^st place in division AUFNIRA (sequential)
• 1^st place in division BV
• 1^st place in division BVFP
• 1^st place in division BVFPLRA
• 1^st place in division FP
• 1^st place in division FPLRA
• 1^st place in division LIA
• 1^st place in division LRA
• 1^st place in division NIA (sequential, parallel, sat, 24s)
• 1^st place in division QF_ABVFPLRA (sequential, parallel, sat, unsat)
• 1^st place in division QF_ANIA
• 1^st place in division QF_AUFNIA
• 1^st place in division QF_BVFPLRA
• 1^st place in division QF_DT
• 1^st place in division QF_IDL (unsat)
• 1^st place in division QF_LIA (sequential, parallel, sat)
• 1^st place in division QF_NIA (sequential, parallel, sat)
• 1^st place in division QF_S
• 1^st place in division QF_SLIA
• 1^st place in division QF_UFNIA (sequential, parallel, unsat, 24s)
• 1^st place in division UF (unsat)
• 1^st place in division UFBV
• 1^st place in division UFDT (sequential, parallel, sat, unsat)
• 1^st place in division UFDTLIA (sequential, parallel, unsat)
• 1^st place in division UFDTLIRA (sequential, parallel, sat, 24s)
• 1^st place in division UFDTNIRA (sequential, 24s)
• 1^st place in division UFFPDTLIRA
• 1^st place in division UFFPDTNIRA
• 1^st place in division UFIDL
• 1^st place in division UFLIA (sequential, parallel, unsat, 24s)
• 1^st place in division UFNIA

Incremental Track

• 1^st place in division ANIA
• 1^st place in division AUFNIRA
• 1^st place in division BV
• 1^st place in division BVFP
• 1^st place in division LRA
• 1^st place in division QF_FP
• 1^st place in division QF_NIA
• 1^st place in division QF_UFNIA
• 1^st place in division UF
• 1^st place in division UFLRA
• 1^st place in division UFNIA
• 1^st place in division UFNRA

Model Validation Track

• 1^st place in division QF_LIA

Unsat Core Track

• 1^st place in division AUFBVDTLIA
• 1^st place in division AUFDTLIRA
• 1^st place in division AUFDTNIRA
• 1^st place in division AUFFPDTLIRA
• 1^st place in division AUFLIA
• 1^st place in division AUFLIRA
• 1^st place in division AUFNIRA
• 1^st place in division BV
• 1^st place in division LIA
• 1^st place in division QF_ALIA
• 1^st place in division QF_AUFLIA
• 1^st place in division QF_UFLRA
• 1^st place in division UF
• 1^st place in division UFDT
• 1^st place in division UFDTLIRA
• 1^st place in division UFDTNIRA
• 1^st place in division UFFPDTLIRA
• 1^st place in division UFFPDTNIRA
• 1^st place in division UFIDL
• 1^st place in division UFLIA
• 1^st place in division UFNIA

Competition-Wide Awards

---

Biggest Lead

• 1^st place in the Single Query Track (sequential, parallel, sat, unsat, 24s)
• 1^st place in the Incremental Track
• 1^st place in the Unsat Core Track (sequential, parallel)

Largest Contribution

• 1^st place in the Single Query Track (sequential, parallel, sat)
• 1^st place in the Incremental Track
• 1^st place in the Unsat Core Track (sequential, parallel)