CVC4 at SMT-COMP 2019

---

SMT-COMP 2019

Competing Version:  GitHub Branch smtcomp2019
System Description:  CVC4 at the SMT-COMP 2019

Tracks Entered

---

• Single Query Track
  Divisions:  all divisions (51)
  Competing Binary:  StarExec Binary
• Incremental Track
  Divisions:  all divisions (24)
  Competing Binary:  StarExec Binary
• Challenge Track (non-incremental)
  Divisions:  all divisions (3)
  Competing Binary:  StarExec Binary
• Challenge Track (incremental)
  Divisions:  all divisions (3)
  Competing Binary:  StarExec Binary
• Unsat Core Track
  Divisions:  all divisions (33)
  Competing Binary:  StarExec Binary
• Model Validation Track
  Divisions:  all divisions (1)
  Competing Binary:  StarExec Binary

Track Awards

---

Single Query Track

• 1^st place in division ABVFP
• 1^st place in division ALIA (24s)
• 1^st place in division AUFDTLIA
• 1^st place in division AUFLIA (sequential, sat)
• 1^st place in division BVFP
• 1^st place in division FP
• 1^st place in division LIA
• 1^st place in division NIA
• 1^st place in division QF_ANIA (sequential, parallel, unsat)
• 1^st place in division QF_DT
• 1^st place in division QF_UFNIA
• 1^st place in division UF (sequential)
• 1^st place in division UFDT (sequential, parallel, sat, unsat)
• 1^st place in division UFDTLIA (sequential, parallel, unsat)

Incremental Track

• 1^st place in division ABVFP
• 1^st place in division ALIA
• 1^st place in division ANIA
• 1^st place in division AUFNIRA
• 1^st place in division BV
• 1^st place in division QF_ANIA
• 1^st place in division UFLRA

Unsat Core Track

• 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_ANIA
• 1^st place in division QF_AUFLIA
• 1^st place in division QF_NRA
• 1^st place in division QF_UFLRA
• 1^st place in division UF
• 1^st place in division UFIDL
• 1^st place in division UFLIA
• 1^st place in division UFLRA
• 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)