usi-verification-and-security / opensmt

The opensmt solver
Other
78 stars 18 forks source link

Improve Handling of Empty Name in Logic::mkConst #695

Closed merlinsun closed 7 months ago

merlinsun commented 8 months ago

Fixes #694.

When opensmt processes assertions involving empty name, it triggers an assertion failure in Logic::mkConst.

To resolve this issue, I propose a modification to the Logic::mkConst to check for empty name explicitly. If an empty name is encountered, the function will now print an error message and return PTRef_Undef.