Logo

An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

View on GitHub
Downloads
Documentation
People
Publications
Awards
Third Party Applications
Acknowledgements

Try cvc5 online!

License: BSD
CI
Coverage

SMT-COMP 2021

https://smt-comp.github.io/2021

System Description:  cvc5 at the SMT Competition 2021
Submitted Binaries:

Divisions Entered

Division Awards

Single Query Track

https://smt-comp.github.io/2021/results/results-single-query

  1st place in division Arith (sequential, parallel, sat, 24s)
  1st place in division Bitvec (all)
  1st place in division Equality+LinearArith (all)
  1st place in division Equality+MachineArith (all)
  1st place in division Equality+NonLinearArith (unsat)
  1st place in division Equality (unsat)
  1st place in division FPArith (all)
  1st place in division QF_Equality+LinearArith (unsat)
  1st place in division QF_Equality+NonLinearArith (all)
  1st place in division QF_Equality (sequential, parallel, sat, unsat)
  1st place in division QF_FPArith (all)
  1st place in division QF_LinearIntArith (sequential, parallel, sat, unsat)
  1st place in division QF_LinearRealArith (unsat)
  1st place in division QF_NonLinearIntArith (sequential, parallel, sat)
  1st place in division QF_NonLinearRealArith (all)
  1st place in division QF_Strings (all)

Incremental Track

https://smt-comp.github.io/2021/results/results-incremental

  1st place in division Arith (all)
  1st place in division Bitvec (all)
  1st place in division Equality+LinearArith (all)
  1st place in division Equality (all)
  1st place in division FPArith (all)
  1st place in division QF_Equality+LinearArith (all)
  1st place in division QF_Equality (all)

Model Validation Track

https://smt-comp.github.io/2021/results/results-model-validation

  1st place in division QF_LinearIntArith (all)

Unsat Core Track

https://smt-comp.github.io/2021/results/results-unsat-core

  1st place in division Arith (all)
  1st place in division Bitvec (all)
  1st place in division Equality+LinearArith (all)
  1st place in division Equality+MachineArith (all)
  1st place in division Equality+NonLinearArith (all)
  1st place in division Equality (all)
  1st place in division FPArith (all)
  1st place in division QF_Equality+NonLinearArith (all)
  1st place in division QF_Equality (all)
  1st place in division QF_LinearIntArith (all)
  1st place in division QF_NonLinearIntArith (all)
  1st place in division QF_NonLinearRealArith (all)

Biggest Lead

  1st place (gold) in the Incremental Track (all)
  1st place (gold) in the Model Validation Track (all)
  1st place (gold) in the Single Query Track (all)
  1st place (gold) in the Unsat Core Track (all)

Largest Contribution

  1st place (gold) in the Incremental Track (all)
  1st place (gold) in the Model Validation Track (all)
  1st place (gold) in the Single Query Track (sat, unsat)
  1st place (gold) in the Unsat Core Track (all)
  2nd place (silver) in the Single Query Track (sequential, 24s)
  3rd place (bronze) in the Single Query Track (parallel)