search

chipmunk-project / chipmunk

A code generator for packet-processing pipelines based on end-to-end program synthesis
12 stars 5 forks source link

Bug in SKETCH's generation of smt2 file. #161

Closed anirudhSK closed 5 years ago

anirudhSK commented 5 years ago

As @taegyunkim pointed out here: https://lists.csail.mit.edu/pipermail/sketchusers/2019-July/000092.html, there's a bug in the way the smt2 file is generated.

This is causing several unit tests to fail during CI, e.g., https://github.com/chipmunk-project/chipmunk/pull/160 and https://github.com/chipmunk-project/chipmunk/pull/157.

taegyunkim commented 5 years ago

https://bitbucket.org/gatoatigrado/sketch-backend/src/7cdf7bda081649bfc101ec506f1e1caf34cb5b05/src/SketchSolver/InputParser/BooleanDAG.cpp#lines-966

@anirudhSK this is the code that generates SMT2 file within sketch-backend.

anirudhSK commented 5 years ago

This is a similar, but different, error: https://lists.csail.mit.edu/pipermail/sketchusers/2019-August/000096.html