Aina Niemetz

Sr. Research Scientist, Computer Science
Stanford University

           

Publications
Talks
Tools
Awards

cvc5 at SMT-COMP 2024

https://smt-comp.github.io/2024
https://cvc5.github.io

Single Query Track

Results: https://smt-comp.github.io/2024/results/results-single-query
Awards: sequential (seq), parallell (par), sat, unsat, 24s

  1st place in division Arith (seq, par, unsat)
  1st place in division Bitvec (seq, par, unsat)
  1st place in division Equality (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 QF_Datatypes (sat)
  1st place in division QF_Equality+NonLinearArith (unsat)
  1st place in division QF_LinearIntArith (unsat)
  1st place in division QF_LinearRealArith (unsat)
  1st place in division QF_NonLinearRealArith (unsat)

Incremental Track

Results: https://smt-comp.github.io/2024/results/results-incremental
Awards: parallell (par), 24s

  1st place in division Arith (par)
  1st place in division Bitvec (par)
  1st place in division Equality (all)
  1st place in division Equality+LinearArith (all)
  1st place in division Equality+NonLinearArith (all)
  1st place in division FPArith (24s)
  1st place in division QF_Equality+NonLinearArith (par)

Unsat Core Track

Results: https://smt-comp.github.io/2024/results/results-unsat-core
Awards: sequential (seq), parallell (par), unsat, 24s

  1st place in division Arith (all)
  1st place in division Bitvec (all)
  1st place in division Equality (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 QF_Datatypes (seq, par, unsat)
  1st place in division QF_Equality+BitVec (seq, par, unsat)
  1st place in division QF_Equality+NonLinearArith (all)
  1st place in division QF_NonLinearIntArith (all)
  1st place in division QF_NonLinearRealArith (all)

Biggest Lead

  1st place (gold) in the Single Query Track (seq, par, sat, unsat)
  1st place (gold) in the Unsat Core Track (all)
  2nd place (silver) in the Single Query Track (24s)

Largest Contribution

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