search

mattulbrich / llreve

Automatic regression verification for LLVM programs
http://formal.iti.kit.edu/reve
Other
19 stars 6 forks source link

Z3 output broken in the presence of extern functions #18

Closed cocreature closed 7 years ago

cocreature commented 7 years ago

Extern functions include implications. This results in non-Horn clauses being output which Z3 does not handle correctly.

cocreature commented 7 years ago

It looks like this is not a problem after all and the bug I’m seeing is caused by something else.