Skip to content
This repository has been archived by the owner on Aug 23, 2024. It is now read-only.

Bug in scope handling (SMT-LIB 2 parser) #21

Closed
pkreutzer opened this issue Oct 25, 2018 · 2 comments
Closed

Bug in scope handling (SMT-LIB 2 parser) #21

pkreutzer opened this issue Oct 25, 2018 · 2 comments
Assignees
@mpreiner

Comments

@pkreutzer
Copy link

pkreutzer commented Oct 25, 2018 •
edited
Loading

Hi there,

we observed a bug with the following (already reduced) SMT-LIB 2 script:

(set-logic QF_UFBV)
(push 2)
(declare-fun t_n () (_ BitVec 27))
(check-sat)
(pop 1)
(declare-fun t_n (Bool Bool) (_ BitVec 3))
(check-sat)
(exit)

Using both the most recent version and the version tagged 3.0.0, Boolector prints the following error:

[boolector] boolector_uf: symbol 'BTOR@2t_n' is already in use

The bug seems to be related to the scope handling in the SMT-LIB 2 parser. If we apply the following patch, the bug disappears: boolector-3.0.0.patch.txt Sorry, but the patch does not work properly. If we add (push 1) after the pop command, Boolector prints an error message again. It seems that the symbol table is not properly cleared when leaving the scope, but this is just an assumption...
@mpreiner
Copy link
Member

Thanks for the bug report, we'll have a look at it!

@mpreiner mpreiner self-assigned this Oct 29, 2018
mpreiner added a commit that referenced this issue Oct 30, 2018
@mpreiner
Fix context-unique symbols.
1f0c288 
Uniqueness of symbols in current context is now ensured on API level rather
than SMT2 front-end level.

Fixes #21.
@mpreiner
Copy link
Member

This issue is now fixed on master, let us know if you run into any other issues.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees

@mpreiner mpreiner

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@mpreiner @pkreutzer