Aina Niemetz

Sr. Research Scientist, Computer Science
Stanford University

           

Publications
Talks
Tools
Awards

cvc5 at SMT-COMP 2023

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

Single Query Track

Results: https://smt-comp.github.io/2023/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 (seq, par, sat, unsat)
  1st place in division Equality+LinearArith (all)
  1st place in division Equality+MachineArith (all)
  1st place in division Equality+NonLinearArith (seq, par, unsat, 24s)
  1st place in division QF_Datatypes (seq, par, sat, unsat)
  1st place in division QF_Equality+NonLinearArith (all)
  1st place in division QF_LinearIntArith (unsat)
  1st place in division QF_LinearRealArith (unsat)
  1st place in division QF_NonLinearRealArith (unsat, 24s)
  1st place in division QF_Strings (seq, par, sat, unsat)

Honorable Mentions

In division Arith:
  1st place in logic LIA (sat, 24s)
  1st place in logic NIA (sat, 24s)

In division Equality:
  1st place in logic UFDT (24s)

In division QF_Equality+NonLinearArith:
  1st place in logic QF_UFNIA (sat)

In division QF_FPArith:
  1st place in logic QF_FP (sat)

In division QF_LinearIntArith:
  1st place in logic QF_UFDTLIRA (all)

In division QF_NonLinearIntArith:
  1st place in logic QF_NIRA (seq, par, unsat)

In division QF_Equality+Bitvec:
  1st place in logic QF_UFBVDT (all)

Incremental Track

Results: https://smt-comp.github.io/2023/results/results-incremental
Awards: parallell (par)

  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+NonLinearArith (all)
  1st place in division QF_Equality (all)
  1st place in division QF_Equality+BitVec+Arith (all)
  1st place in division QF_Equality+NonLinearArith (all)

Honorable Mentions

In division QF_Equality+LinearArith:
  1st place in logic QF_ALIA (all)

In division QF_FPArith:
  1st place in logic QF_BVFPLRA (all)

Unsat Core Track

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

  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)
  1st place in division QF_Equality+NonLinearArith (all)
  1st place in division QF_FPArith (all)

Honorable Mentions

In division QF_Equality+LinearArith:
  1st place in logic QF_AUFLIA (all)
  1st place in logic QF_UFLRA (all)

In division QF_LinearIntArith:
  1st place in logic QF_IDL (all)
  1st place in logic QF_UFDTLIRA (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)