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

NullPointerException at SimpleAPI.scala:4116 #10

Open
rainoftime opened this issue Jul 20, 2020 · 0 comments
Open

NullPointerException at SimpleAPI.scala:4116 #10

rainoftime opened this issue Jul 20, 2020 · 0 comments
Labels
issues with princess Issue not due to OSTRICH, but the underlying SMT solver

Comments

@rainoftime
Copy link

rainoftime commented Jul 20, 2020

Hi, for the following instance

(set-logic NIA)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const i1 Int)
(declare-const i5 Int)
(declare-const i8 Int)
(declare-const i11 Int)
(declare-const v7 Bool)
(assert (=> (>= 68 i8) v6))
(declare-const i13 Int)
(declare-const v8 Bool)
(assert v7)
(check-sat)
(assert (exists ((q0 Bool) (q1 Bool) (q2 Bool) (q3 Int)) (=> (distinct q1 q1 v0 (=> (>= 68 i8) v6) (distinct 7 68) q0 v4 q1) (>= i13 q3))))
(assert (exists ((q0 Bool) (q2 Bool) ) (forall ((q1 Bool) (q3 Int) ) (=> (>= q3 q3) (xor q2 q1 v6)))))
(push 1)
(assert (exists ((q4 Bool) (q5 Bool) (q6 Int)) (not (xor (<= 930 7) q4 q5 q4 q4 q5 (or (xor v7 v2 v3 v0 v7 v5 (< i11 i5) v3) v2 v4 (< i11 i5) v2 v4 v4 v4 (>= 68 i8) v4) q4 q4 (>= 68 i8)))))
(assert (< i11 i5))
(push 1)
(assert (distinct v5 v4))
(check-sat)

ostrich 2b3eb9b

java.lang.NullPointerException
        at ap.SimpleAPI.ap$SimpleAPI$$addToProver(SimpleAPI.scala:4116)
        at ap.SimpleAPI.flushTodo(SimpleAPI.scala:4059)
        at ap.SimpleAPI.pushHelp(SimpleAPI.scala:3930)
        at ap.SimpleAPI.push(SimpleAPI.scala:3925)
        at ap.parser.SMTParser2InputAbsy.push(SMTParser2InputAbsy.scala:866)
        at ap.parser.SMTParser2InputAbsy.ap$parser$SMTParser2InputAbsy$$apply(SMTParser2InputAbsy.scala:1449)
        at ap.parser.SMTParser2InputAbsy$$anon$1.commandHook(SMTParser2InputAbsy.scala:536)
        at ap.parser.smtlib.CUP$parser$actions.CUP$parser$do_action(parser.java:1289)
        at ap.parser.smtlib.parser.do_action(parser.java:419)
        at java_cup.runtime.lr_parser.parse(lr_parser.java:584)
        at ap.parser.smtlib.parser.pScriptC(parser.java:441)
        at ap.parser.SMTParser2InputAbsy.processIncrementally(SMTParser2InputAbsy.scala:548)
        at ap.CmdlMain$$anonfun$7.apply(CmdlMain.scala:565)
        at ap.CmdlMain$$anonfun$7.apply(CmdlMain.scala:563)
        at ap.SimpleAPI$.withProver(SimpleAPI.scala:169)
        at ap.CmdlMain$.proveMultiSMT(CmdlMain.scala:563)
        at ap.CmdlMain$.proveProblems(CmdlMain.scala:595)
        at ap.CmdlMain$$anonfun$doMain$2.apply(CmdlMain.scala:931)
        at ap.CmdlMain$$anonfun$doMain$2.apply(CmdlMain.scala:929)
        at scala.collection.mutable.ResizableArray$class.foreach(ResizableArray.scala:59)
        at scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:48)
        at ap.CmdlMain$.doMain(CmdlMain.scala:929)
        at ap.CmdlMain$.main(CmdlMain.scala:879)
        at ap.CmdlMain.main(CmdlMain.scala)

@pruemmer pruemmer added the issues with princess Issue not due to OSTRICH, but the underlying SMT solver label Jul 11, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
issues with princess Issue not due to OSTRICH, but the underlying SMT solver
Projects
None yet
Development

No branches or pull requests

2 participants