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

(produce-abducts) Fatal failure at src/theory/eager_proof_generator.cpp:35 #6605

Closed
zhendongsu opened this issue May 22, 2021 · 4 comments
Closed

(produce-abducts) Fatal failure at src/theory/eager_proof_generator.cpp:35 #6605

zhendongsu opened this issue May 22, 2021 · 4 comments
Assignees
@HanielB @ajreynol

Comments

@zhendongsu
Copy link

Commit: 0e9fed3
OS: Ubuntu 18.04

[532] % cvc4-1.8 -q --check-unsat-cores small.smt2
(define-fun d () Bool (= b a))
[533] % cvc5 -q --check-unsat-cores small.smt2
Fatal failure within void cvc5::theory::EagerProofGenerator::setProofFor(cvc5::Node, std::shared_ptr<cvc5::ProofNode>) at /local/suz-local/software/CVC4/src/theory/eager_proof_generator.cpp:35
Check failure

 pf->getResult() == f
EagerProofGenerator::setProofFor: unexpected result
Expected: (>= rsk_11 1)
Actual: (not (not (>= rsk_11 1)))

Aborted
[534] % 
[534] % cat small.smt2
(set-option :produce-abducts true)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (= (>= b c) (>= 0 a)))
(assert (= c a))
(get-abduct d (<= a b))
[535] %
@rainoftime
Copy link

rainoftime commented May 23, 2021 •
edited

src/smt/abduction_solver.cpp:108

(get-abduct A true)

cvc5  -q -i --produce-abducts delta.out.smt2 
Fatal failure within bool cvc5::smt::AbductionSolver::getAbductInternal(cvc5::Node&) at /home/cvc5/src/smt/abduction_solver.cpp:108
Check failure

 !agdtbv.isNull()

Aborted

@rainoftime
Copy link

src/theory/uf/equality_engine.cpp:585

(declare-sort S0 0)
(declare-sort S2 0)
(declare-fun arr0 () (Array Bool S2))
(declare-fun arr1 () (Array S2 (Array S0 (Array S0 (Array S0 Bool)))))
(declare-fun arr2 () (Array Bool (Array Bool (Array S0 (Array S0 (Array S0 Bool))))))
(get-abduct A (= (select (select arr2 false) true) (select arr1 (select arr0 false))))

cvc5 -q --produce-abducts x.smt2 
Fatal failure within cvc5::TNode cvc5::theory::eq::EqualityEngine::getRepresentative(cvc5::TNode) const at /home/cvc5/src/theory/uf/equality_engine.cpp:585
Check failure

 hasTerm(t)

Aborted

@ajreynol
Copy link
Member

ajreynol commented May 27, 2021 •
edited

Last one appears to be specific to arrays solver:

#0  0x000000000135da95 in raise ()
#1  0x000000000040494d in abort ()
#2  0x00000000008b74ca in cvc5::FatalStream::~FatalStream (this=this@entry=0x7fffffffb5ff, __in_chrg=<optimized out>) at /space/ajreynol/cvc5-ajr/src/base/check.cpp:32
#3  0x000000000074ddd5 in cvc5::theory::eq::EqualityEngine::getRepresentative (this=this@entry=0x1f55c88, t=...) at /space/ajreynol/cvc5-ajr/src/theory/uf/equality_engine.cpp:587
#4  0x000000000053d3fd in cvc5::theory::arrays::TheoryArrays::mergeArrays (this=this@entry=0x1f55120, a=..., b=...)
    at /space/ajreynol/cvc5-ajr/src/theory/arrays/theory_arrays.cpp:1563
#5  0x000000000054fab6 in cvc5::theory::arrays::TheoryArrays::NotifyClass::eqNotifyMerge (this=this@entry=0x1f56370, t1=..., t2=...)
    at /space/ajreynol/cvc5-ajr/src/./theory/arrays/theory_arrays.h:341
#6  0x000000000075a2a4 in cvc5::theory::eq::EqualityEngine::merge (this=this@entry=0x204c5c0, class1=..., class2=..., triggersFired=...)
    at /space/ajreynol/cvc5-ajr/src/theory/uf/equality_engine.cpp:744
...

@ajreynol ajreynol mentioned this issue May 27, 2021
Merged
HanielB pushed a commit that referenced this issue May 27, 2021
@ajreynol
Fix spurious assertion for trivial abduction (#6629)
8d63f44 
Fixes 2nd benchmark from #6605.
This was referenced Oct 19, 2021
Merged
Merged
aniemetz pushed a commit that referenced this issue Oct 20, 2021
@ajreynol
Check whether abduct option is enabled (#7418)
221f8b4 
This addresses one of the issues related to #6605.
ajreynol added a commit that referenced this issue Oct 20, 2021
@ajreynol
Make SyGuS solver robust to non-closed enumerable sorts (#7417)
628a13f 
This makes the SyGuS solver robust to variables that are not closed enumerable, e.g. arrays of uninterpreted sorts.

It corrects an issue in array's mkGroundTerm issue which would allow constants to enter into constraints for SyGuS problems with arrays. This method does not cause further issues currently since quantifiers is guarded in several places to ensure array constants are not constructed via this method.

It also makes it so that we don't add explicit CEGIS refinement lemmas unless evaluation unfolding is enabled and the counterexamples are from closed enumerable types; there is no reason to add these unless we are combining with evaluation unfolding.

This addresses several of the issues raised in #6605.
@ajreynol
Copy link
Member

ajreynol commented Oct 22, 2021 •
edited

This issue is fixed due to a combination of the last 2 referenced PRs.

@ajreynol ajreynol mentioned this issue Oct 22, 2021
Merged
ajreynol added a commit that referenced this issue Oct 22, 2021
@ajreynol
Add more abduction regressions (#7461)
4929b5d 
Fixes #5848.

This also fixes an issue leftover from #6605 where a spurious assertion failure was thrown.

Also introduces subfolder regress/regress1/abduction.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@HanielB HanielB

@ajreynol ajreynol

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@rainoftime @HanielB @ajreynol @zhendongsu