Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

snorm-infer-eq fatal failure at src/theory/quantifiers/equality_infer.cpp:144 #3955

Closed
rainoftime opened this issue Mar 9, 2020 · 1 comment · Fixed by #4036
Closed

snorm-infer-eq fatal failure at src/theory/quantifiers/equality_infer.cpp:144 #3955

rainoftime opened this issue Mar 9, 2020 · 1 comment · Fixed by #4036
Assignees
@ajreynol

Comments

@rainoftime
Copy link

rainoftime commented Mar 9, 2020 •
edited

Hi,
For this formula:
equality_infer144.txt

CVC4 incremenal mode throws out a fatal failure:

Fatal failure within void CVC4::theory::quantifiers::EqualityInference::eqNotifyNewClass(CVC4::TNode) at /home/peisen/test/tofuzz/CVC4/src/theory/quantifiers/equality_infer.cpp:144
Check failure

 !eqci->d_valid.get()

Aborted (core dumped)

OS: Ubuntu 16.04
Commit: a0b35a8
@ajreynol ajreynol self-assigned this Mar 9, 2020
@ajreynol
Copy link
Member

ajreynol commented Mar 9, 2020

Caused by getting a duplicate eqNotifyNewEqClass notification from the congruence manage of arithmetic.

This was referenced Mar 10, 2020
Closed
Merged
4tXJ7f pushed a commit that referenced this issue Mar 12, 2020
@ajreynol
Fix double notify in equality engine (#4036)
08431f8 
Fixes #3955.

Previously we were getting two calls to notifyNewEqClass from the equality engine for new application nodes, since the notification was being done in an internal call to newNode(...). The proper place to call this is in addTermInternal(...) which is called only once per Node per SAT context.

This bug potentially impacted some performance (due to redundant calls), and also broke the contract that notifyNewEqClass should only be called once per node per SAT context. In most cases, this was being handled in a benign way by theory solvers, although an assertion was failing in EqualityQuery, which is fixed by this PR.

A block of code changed indentation in this commit.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@ajreynol ajreynol

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix double notify in equality engine ajreynol/CVC4
2 participants
@rainoftime @ajreynol