The 28 btr files in comp/2018/General_Track/ and their byte-identical copies in comp/2017/General_Track/ contain line-3 Expected solution annotations. Four say any; the other 24 give concrete formulas.
All 24 concrete formulas omit the shift-count mask required by their own specifications:
For example, btr-solution-3.sl suggests x & ~(1 << bit). With x = 0x00000001 and bit = 0x00000020, the specification masks the shift count to zero and returns 0x00000000; the annotated formula shifts by 32 and returns 0x00000001. The same input distinguishes all 24 concrete annotations from their specifications.
The maintained SyGuS 2.0 copies in lib/General_Track/from_2018/ do not contain these annotations, so the current benchmark specifications are unaffected. I also verified that all 28 benchmarks remain realizable within their respective grammars.
I am not requesting changes to the archived comp/ files; I am filing this as a searchable erratum.
The 28
btrfiles incomp/2018/General_Track/and their byte-identical copies incomp/2017/General_Track/contain line-3Expected solutionannotations. Four sayany; the other 24 give concrete formulas.All 24 concrete formulas omit the shift-count mask required by their own specifications:
For example,
btr-solution-3.slsuggestsx & ~(1 << bit). Withx = 0x00000001andbit = 0x00000020, the specification masks the shift count to zero and returns0x00000000; the annotated formula shifts by 32 and returns0x00000001. The same input distinguishes all 24 concrete annotations from their specifications.The maintained SyGuS 2.0 copies in
lib/General_Track/from_2018/do not contain these annotations, so the current benchmark specifications are unaffected. I also verified that all 28 benchmarks remain realizable within their respective grammars.I am not requesting changes to the archived
comp/files; I am filing this as a searchable erratum.