CVC4 at SMT-COMP 2015

---

SMT-COMP 2015

Competing Versions:

• GitHub Branch smtcomp2015-stable (CVC4 (master))
• GitHub Branch smtcomp2015-experimental (CVC4 (experimental))

System Description:  SMT-COMP 2015 entry: CVC4 v1.5-prerelease

Tracks Entered

---

• Main Track
  Divisions:  all divisions except FP logics (38, 10 non-competitive)
  Competing Binaries:
  • CVC4 (master)
  • CVC4 (experimental)
• Application Track
  Divisions:  all divisions (14, 8 non-competitive)
  Competing Binaries:
  • CVC4-app (master)
  • CVC4-app (experimental)

Track Awards

---

Main Track

  1^st place in division ALIA (all)
  1^st place in division AUFLIA (all)
  1^st place in division AUFLIRA (all)
  1^st place in division AUFNIRA (all)
  1^st place in division LRA (all)
  1^st place in division NRA (all)
  1^st place in division QF_AUFBV (all)
  1^st place in division QF_LIA (sequential, sequential industrial) (all)
  1^st place in division QF_LRA (all)
  1^st place in division QF_NIRA (all)
  1^st place in division QF_UFNIA (all)
  1^st place in division UF (all)
  1^st place in division UFIDL (all)
  1^st place in division UFLIA (all)
  1^st place in division UFNIA (all)

Application Track

  1^st place in division LIA (all)
  1^st place in division QF_UFLIA (all)
  1^st place in division QF_UFNIA (all)

Competition-Wide Awards

---

Sequential Performance

  1^st place in the Main Track

Sequential Performance (industrial)

  1^st place in the Main Track

Parallel Performance

  1^st place in the Main Track

Parallel Performance (industrial)

  1^st place in the Main Track