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.

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

[Consolidated] Issues related to interpolant #255

Open
rainoftime opened this issue Feb 4, 2021 · 2 comments
Open

[Consolidated] Issues related to interpolant #255

rainoftime opened this issue Feb 4, 2021 · 2 comments
Assignees

Comments

@rainoftime
Copy link

rainoftime commented Feb 4, 2021

src/./expr/node_builder.h:960

(get-interpol I false)
cvc4 -q  --produce-interpols=default delta.out.smt2 
Fatal failure within CVC4::expr::NodeValue* CVC4::NodeBuilder<N>::constructNV() [with unsigned int nchild_thresh = 10u] at CVC4/src/./expr/node_buildeCr.h:960
Check failure

 getNumChildren() >= kind::metakind::getLowerBoundForKind(getKind())
Nodes with kind BOUND_VAR_LIST must have at least 1 children (the one under construction has 0)
Aborted

ac998a45ae64

@rainoftime
Copy link
Author

rainoftime commented Feb 4, 2021

src/./expr/node_value.h:496

(declare-fun v0 () Bool)
(assert v0)
(get-interpol I (or v0 true))
cvc4 -q  --produce-interpols=default delta.out.smt2 
Fatal failure within CVC4::expr::NodeValue* CVC4::expr::NodeValue::getChild(int) const at CVC4/src/./expr/node_value.h:496
Check failure

 i >= 0 && unsigned(i) < d_nchildren

Aborted

@rainoftime
Copy link
Author

src/theory/theory_engine.cpp:878

(set-logic QF_ALIA)
(declare-sort S0 0)
(declare-sort S1 0)
(declare-sort S3 0)
(declare-fun v9 () Bool)
(declare-fun v98 () Bool)
(declare-fun arr--6415793657884950151_-6415793657884950151-0 () (Array Bool Bool))
(declare-fun arr--6415793657884950151_830186755938822928-1 () (Array Bool S1))
(declare-fun arr--6415793657884950151_830186755937740403-0 () (Array Bool S0))
(declare-fun arr-830186755937740403_-6415793657884950151-0 () (Array S0 Bool))
(declare-fun arr-8998691489526778111_830186755938822928-0 () (Array Int S1))
(declare-fun arr-8998691489526778111_830186755940987978-0 () (Array Int S3))
(declare-fun arr-830186755938822928_830186755937740403-0 () (Array S1 S0))
(declare-fun arr--6415793657884950151_2464596404674444697-0 () (Array Bool (Array Int S1)))
(declare-fun arr-830186755937740403_-6244198113904750524-0 () (Array S0 (Array S3 (Array Bool (Array Int S1)))))
(assert (xor true true true true true (not (select arr-830186755937740403_-6415793657884950151-0 (select arr--6415793657884950151_830186755937740403-0 false)))))
(get-interpol I (and v9 (= arr--6415793657884950151_2464596404674444697-0 (select (select arr-830186755937740403_-6244198113904750524-0 (select (store arr-830186755938822928_830186755937740403-0 (select arr--6415793657884950151_830186755938822928-1 false) (select (store (store arr--6415793657884950151_830186755937740403-0 v9 (select arr--6415793657884950151_830186755937740403-0 false)) v98 (select arr--6415793657884950151_830186755937740403-0 (select arr--6415793657884950151_-6415793657884950151-0 true))) true)) (select arr-8998691489526778111_830186755938822928-0 1))) (select arr-8998691489526778111_830186755940987978-0 0)))))
cvc4 -q  --produce-interpols=default delta.out.smt2 
Fatal failure within void CVC4::TheoryEngine::assertToTheory(CVC4::TNode, CVC4::TNode, CVC4::theory::TheoryId, CVC4::theory::TheoryId) at CVC4/src/theory/theory_engine.cpp:878
Check failure

 toTheoryId != fromTheoryId

Aborted

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants