SMT competitions

---

SMT Competition 2019

• Competing Version: GitHub branch smtcomp19
• System Description: Boolector at the SMT competition 2019
• Divisions Entered:
  • Single Query Track:  BV, QF_ABV, QF_AUFBV, QF_BV, QF_UFBV
  • Incremental Track:  QF_ABV, QF_AUFBV, QF_BV, QF_UFBV
  • Challenge Track (non-incremental):  QF_ABV, QF_AUFBV, QF_BV
  • Challenge Track (incremental):  QF_ABV, QF_AUFBV, QF_BV
  • Model Validation Track:  QF_BV
• Awards:
  • Single Query Track
    • 1^st place in division QF_ABV (sequential, sat)
    • 1^st place in division QF_BV (sequential, parallel, sat, unsat)
  • Challenge Track
    • 1^st place in division QF_ABV [non-incrementa] (sequential, parallel, sat, 24s)
    • 1^st place in division QF_ABV [incremental] (all)
    • 1^st place in division QF_AUFBV [non-incremental] (unsat)
    • 1^st place in division QF_BV [non-incremental] (sequential)
    • 1^st place in division QF_BV [incremental] (all)
  • Model Validation Track
    • 1^st place in division QF_BV (all)
  • Biggest Lead
    • 2^nd place (silver) in the Challenge Track [incremental] (all)
    • 1^st place (gold) in the Challenge Track [non-incremental] (unsat)
    • 2^nd place (silver) in the Challenge Track [non-incremental] (sequential, 24s)
    • 1^st place in the Model Validation Track [experimental] (all)
  • Largest Contribution
    • 2^nd place (silver) in the Incremental Track (all)
    • 1^st place (gold) in the Challenge Track [non-incremental] (unsat)
    • 2^nd place (silver) in the Challenge Track [non-incremental] (sequential, parallel, sat)
    • 2^nd place (silver) in the Challenge Track [incremental] (all)
    • 1^st place in the Model Validation Track [experimental] (all)
  • 3 silver trophies for Biggest Lead in the Challenge track, and Largest Contribution in the Challenge and Incremental track

---

SMT Competition 2018

• Competing Version: Boolector 3.0
• System Description: Boolector at the SMT competition 2018
• Divisions Entered:
  • Main Track:  BV, QF_ABV, QF_AUFBV, QF_BV, QF_UFBV
  • Application Track:  QF_BV, QF_ABV, QF_UFBV
• Awards:
  • Main Track:
    • 1^st place in QF_ABV (all)
    • 1^st place in QF_BV (sequential)
    • 1^st place in QF_UFBV (all)
  • Application Track:
    • 1^st place in QF_ABV (all)
    • 1^st place in QF_UFBV (all)
  • One Medal in the FLoC’18 Olympic Games
  • Amazon Award

---

SMT Competition 2017

• Competing Version: Boolector 3.0-pre
• System Description: Boolector at the SMT Competition 2017
• Divisions Entered:
  • Main Track:  BV, QF_ABV, QF_AUFBV, QF_BV, QF_UFBV
• Awards:
  • Main Track:
    • 1^st place in QF_ABV (all)
    • 1^st place in QF_BV (sequential)
    • 1^st place in QF_UFBV (all)

---

SMT Competition 2016

• Competing Version: Boolector 2.999
• System Description: Boolector at the SMT Competition 2016
• Divisions Entered:
  • Main Track:  BV, UFBV, QF_ABV, QF_AUFBV, QF_BV, QF_UFBV
• Awards:
  • Main Track:
    • 1^st place in QF_ABV (all)
    • 1^st place in QF_BV (all)
    • 1^st place in QF_UFBV (all)

---

SMT Competition 2015

• Competing Version: Boolector 2.1.0
• System Description: Boolector at the SMT Competition 2015
• Divisions Entered:
  • Main Track:  QF_ABV, QF_AUFBV, QF_BV, QF_UFBV
  • Application Track:  QF_BV
• Awards:
  • Main Track:
    • 1^st place in QF_ABV (all)
    • 1^st place in QF_BV (all)
    • 1^st place in QF_UFBV (all)

---

SMT Competition 2014

• Competing Version: Boolector 2.0.0
• System Description: Boolector at the SMT Competition 2014
• Divisions Entered:
  • Main Track:  QF_ABV, QF_BV
• Awards:
  • Main Track:
    • 1^st place in QF_ABV (all)
    • 1^st place in QF_BV (all)
  • One Gödel Medal in the FLoC’14 Olympic Games

---

No SMT Competition in 2013

---

SMT Competition 2012

• Competing Version: Boolector 1.5.110-agm
• System Description: Boolector at the SMT Competition 2012
• Divisions Entered:
  • Main Track:  QF_AUFBV, QF_BV
• Awards:
  • Main Track:
    • 1^st place in QF_AUFBV
    • 1^st place in QF_BV

---

SMT Competition 2011

• Competing Version: Boolector 1.5.23-833
• Divisions Entered:
  • Main Track:  QF_AUFBV, QF_BV
• Awards:
  • Main Track:
    • 1^st place in QF_AUFBV

---

SMT Competition 2010

no participation

---

SMT Competition 2009

• Competing Version: Boolector 1.2
• Divisions Entered:
  • Main Track:  QF_AUFBV, QF_BV
• Awards:
  • Main Track:
    • 1^st place in QF_AUFBV

---

SMT Competition 2008

• Competing Version: Boolector 0.4
• Divisions Entered:
  • Main Track:  QF_AUFBV, QF_BV
• Awards:
  • Main Track:
    • 1^st place in QF_AUFBV
    • 1^st place in QF_BV