-
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 LRA)
(declare-fun x () Real)
(assert (forall ((y Real)) (=> (> y 0) (>= y x))))
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(get-value (x (+ x 10)))
(exit)
sat
unsupported
(model
(define-fun x () Real (/ 0 1))
)
error
java.lang.AssertionError: assertion failed: Unexpected new symbols or axioms. This might be due to theories not yet loaded in SimpleAPI, consider adding them explicitly using addTheory(...)
at ap.SimpleAPI.ap$SimpleAPI$$toInternalNoAxioms(SimpleAPI.scala:4231)
at ap.SimpleAPI.reduceTerm(SimpleAPI.scala:3458)
at ap.SimpleAPI.evalHelp(SimpleAPI.scala:3282)
at ap.SimpleAPI.evalToTerm(SimpleAPI.scala:3591)
at ap.parser.SMTParser2InputAbsy$$anonfun$41$$anonfun$apply$5.apply(SMTParser2InputAbsy.scala:1555)
at ap.parser.SMTParser2InputAbsy$$anonfun$41$$anonfun$apply$5.apply(SMTParser2InputAbsy.scala:1550)
at scala.collection.immutable.List.map(List.scala:288)
at ap.parser.SMTParser2InputAbsy$$anonfun$41.apply(SMTParser2InputAbsy.scala:1550)
at ap.parser.SMTParser2InputAbsy$$anonfun$41.apply(SMTParser2InputAbsy.scala:1550)
at ap.SimpleAPI.withTimeout(SimpleAPI.scala:686)
at ap.parser.SMTParser2InputAbsy.ap$parser$SMTParser2InputAbsy$$apply(SMTParser2InputAbsy.scala:1549)
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