-
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_LIA)
(declare-fun x () Int)
(assert (> x 7))
(assert (= (mod x (- 5)) 2))
(check-sat)
(get-model)
(get-value (x (mod x (- 5)) (div x (- 5))))
sat
(model
(define-fun x () Int 12)
)
error
java.lang.AssertionError: assertion failed
at scala.Predef$.assert(Predef.scala:156)
at ap.SimpleAPI.evalHelp(SimpleAPI.scala:3297)
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