search

usi-verification-and-security / opensmt

The opensmt solver
Other
77 stars 18 forks source link

Interpret: Respect scope of term names #727

Closed blishko closed 4 months ago

blishko commented 4 months ago

Previously, we just collected information about user-specified term names globally, but according to SMT-LIB, term names are also limited to their stack frame (unless option :global-declarations is set to true).

Here we replace the data structure that stores information about user-specified term names with one that respect the scope of the name definitions.

Fixes #726. Should also resolve the problem reported in #619 with incorrect unsat core reported in incremental setting.

blishko commented 4 months ago

Renamed the files and added a test and an explanation for the unsat core in incremental setting with global declarations.