uuverifiers / ostrich

An SMT Solver for string constraints
Other
33 stars 8 forks source link

Assertion error at SimpleAPI.scala:2283 on QF_S formula #15

Closed rainoftime closed 2 years ago

rainoftime commented 4 years ago

Hi, for the following formula ostrich 2b3eb9b

(set-logic QF_S)
(set-option :produce-models true)
(declare-fun sigmaStar_0 () String)
(declare-fun literal_2 () String)
(declare-fun x_7 () String)
(declare-fun literal_3 () String)
(declare-fun x_6 () String)
(declare-fun literal_4 () String)
(declare-fun literal_5 () String)
(declare-fun x_12 () String)
(declare-fun sigmaStar_13 () String)
(declare-fun x_8 () String)
(declare-fun epsilon () String)
(declare-fun literal_11 () String)
(declare-fun x_15 () String)
(declare-fun literal_16 () String)
(declare-fun x_17 () String)
(declare-fun x_18 () String)
(declare-fun x_14 () String)
(declare-fun x_20 () String)
(declare-fun literal_19 () String)
(declare-fun x_22 () String)
(declare-fun literal_21 () String)
(declare-fun x_23 () String)
(declare-fun literal_24 () String)
(declare-fun x_26 () String)
(declare-fun x_27 () String)
(declare-fun literal_25 () String)
(declare-fun x_28 () String)
(declare-fun x_32 () String)
(declare-fun literal_33 () String)
(declare-fun x_34 () String)
(declare-fun x_31 () String)
(declare-fun x_35 () String)
(declare-fun x_36 () String)
(assert (= literal_2 ""))
(assert (= x_7 (str.++ literal_2 sigmaStar_0)))
(assert (= literal_3 "<tr>
<td class='"))
(assert (= literal_4 "tbl2"))
(assert (= literal_5 "tbl1"))
(assert (or (= x_6 literal_4) (= x_6 literal_5)))
(assert (= x_12 (str.++ literal_3 x_6)))
(assert (= epsilon ""))
(assert (or (= x_8 epsilon)))
(assert (= x_14 (str.replace x_8 "." " ")))
(assert (= literal_11 ""))
(assert (= x_15 (str.++ x_7 literal_11)))
(assert (= literal_16 "><span title="))
(assert (= x_17 (str.++ x_12 literal_16)))
(assert (or (= x_18 x_15) (= x_18 x_14)))
(assert (= x_20 (str.++ x_17 x_18)))
(assert (= literal_19 "</span></td>
<td align='center' width='1%' class='"))
(assert (= x_22 (str.++ literal_19 x_6)))
(assert (= literal_21 "' style='cursor:hand;'>"))
(assert (= x_23 (str.++ x_20 literal_21)))
(assert (= literal_24 " style=white-space:nowrap'>"))
(assert (= x_26 (str.++ x_22 literal_24)))
(assert (= x_27 (str.++ x_23 x_8)))
(assert (= literal_25 "</td>
<td align='center' width='1%' class='"))
(assert (= x_28 (str.++ literal_25 x_6)))
(assert (= x_32 (str.++ x_27 x_26)))
(assert (= literal_33 " style=white-space:nowrap'>\n"))
(assert (= x_34 (str.++ x_28 literal_33)))
(assert (or (= x_31 epsilon)))
(assert (= x_35 (str.++ x_32 x_31)))
(assert (= x_36 (str.++ x_35 x_34)))
(assert (str.in.re x_36 (re.++ (re.* re.allchar) (re.++ (str.to.re "\<SCRIPT") (re.* re.allchar)))))
(check-sat)
(get-model)
 sat
 error
 ap.SimpleAPI$SimpleAPIForwardedException: Internal exception: java.lang.AssertionError: assertion failed
    at ap.SimpleAPI.evalProverResult(SimpleAPI.scala:2283)
    at ap.SimpleAPI.getStatusHelp(SimpleAPI.scala:2242)
    at ap.SimpleAPI.getStatusWithDeadline(SimpleAPI.scala:2192)
    at ap.SimpleAPI.ensureFullModel(SimpleAPI.scala:3072)
    at ap.SimpleAPI.ap$SimpleAPI$$setupTermEval(SimpleAPI.scala:3481)
    at ap.SimpleAPI.partialModelAsFormula(SimpleAPI.scala:3212)
    at ap.parser.SMTParser2InputAbsy$$anonfun$47.apply(SMTParser2InputAbsy.scala:1631)
    at ap.parser.SMTParser2InputAbsy$$anonfun$47.apply(SMTParser2InputAbsy.scala:1631)
    at ap.SimpleAPI.withTimeout(SimpleAPI.scala:686)
    at ap.parser.SMTParser2InputAbsy.ap$parser$SMTParser2InputAbsy$$apply(SMTParser2InputAbsy.scala:1630)
    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)
 Caused by: java.lang.AssertionError: assertion failed
    at scala.Predef$.assert(Predef.scala:156)
    at ap.proof.ModelSearchProver.extractModel$1(ModelSearchProver.scala:711)
    at ap.proof.ModelSearchProver.handleSatGoal(ModelSearchProver.scala:955)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:482)
    at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
pruemmer commented 2 years ago

This is fixed in version 1.2, thanks for the report!