-
Notifications
You must be signed in to change notification settings - Fork 8
Open
Labels
issues with princessIssue not due to OSTRICH, but the underlying SMT solverIssue not due to OSTRICH, but the underlying SMT solver
Description
Hi, for the following formula
ostrich 2b3eb9b
(set-logic QF_LRA)
(check-sat)
(pop 1)
sat
error
java.lang.RuntimeException: Stack empty
at scala.sys.package$.error(package.scala:27)
at scala.collection.mutable.ArrayStack.pop(ArrayStack.scala:118)
at ap.SimpleAPI.popHelp(SimpleAPI.scala:4008)
at ap.SimpleAPI.pop(SimpleAPI.scala:3993)
at ap.parser.SMTParser2InputAbsy.pop(SMTParser2InputAbsy.scala:875)
at ap.parser.SMTParser2InputAbsy$$anonfun$ap$parser$SMTParser2InputAbsy$$apply$4.apply$mcVI$sp(SMTParser2InputAbsy.scala:1456)
at ap.parser.SMTParser2InputAbsy.ap$parser$SMTParser2InputAbsy$$apply(SMTParser2InputAbsy.scala:1455)
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:568)
at ap.CmdlMain$$anonfun$7.apply(CmdlMain.scala:566)
at ap.SimpleAPI$.withProver(SimpleAPI.scala:169)
at ap.CmdlMain$.proveMultiSMT(CmdlMain.scala:566)
at ap.CmdlMain$.proveProblems(CmdlMain.scala:598)
at ap.CmdlMain$$anonfun$doMain$2.apply(CmdlMain.scala:934)
at ap.CmdlMain$$anonfun$doMain$2.apply(CmdlMain.scala:932)
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:932)
at ap.CmdlMain$.main(CmdlMain.scala:882)
at ostrich.OstrichMain$.main(OstrichMain.scala:37)
at ostrich.OstrichMain.main(OstrichMain.scala)
Metadata
Metadata
Assignees
Labels
issues with princessIssue not due to OSTRICH, but the underlying SMT solverIssue not due to OSTRICH, but the underlying SMT solver