usi-verification-and-security / golem

Solver for Constrained Horn Clauses
MIT License
34 stars 7 forks source link

SAT witnesses with invalid function names #27

Closed rodrigo7491 closed 1 year ago

rodrigo7491 commented 1 year ago

For some of the CHC-comp instances, e.g., CHC-LIA-Lin_307 and CHC-LIA-Lin_314, Golem generates witnesses with invalid function names.

CHC-LIA-Lin_307 has functions names as fail$unknown:38, and I get the error syntax error, unexpected TK_KEY, expecting '('. CHC-LIA-Lin_314 has functions names as <Main: void main(JayArray_java_lang_String)>_Block10_6, and I get the error Syntax error at line 4 near :.

After manually enclosing the function names as |funName|, the witnesses can validated by an SMT solver.