ostrich icon indicating copy to clipboard operation
ostrich copied to clipboard

NullPointerException at SimpleAPI.scala:4116

Open rainoftime opened this issue 5 years ago • 0 comments

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)

rainoftime avatar Jul 20 '20 04:07 rainoftime