uuverifiers / ostrich Goto Github PK

View Code? Open in Web Editor NEW

33.0 4.0 8.0 237.47 MB

An SMT Solver for string constraints

License: Other

Scala 83.58% Shell 0.39% SMT 16.03%

smt-solver strings regular-expressions theorem-prover theorem-proving

ostrich's Introduction

OSTRICH

An SMT Solver for String Constraints

OSTRICH is an SMT solver for string constraints.

Using Ostrich

After installing the Scala Build tool (SBT), you can assemble a JAR file using sbt assembly. To run it, use either the ostrich script in the root folder, or ostrich-client. The latter transparently spins up a server that continuously serves requests from the client script; useful to avoid cold-starting the JVM if you are running many instances.

See ./ostrich -help for more options.

The theory behind OSTRICH is explained in the slides of our POPL'24 tutorial.

Web Interface

For experiments, OSTRICH can also be used through its web interface.

Input Format

OSTRICH accepts constraints written using the SMT-LIB theory of strings.

In addition to the standardized SMT-LIB operators, OSTRICH can handle a number of further functions.

Additional string functions

Name	Explanation
str.reverse	Reverse a string

Unary transducers

Finite-state transducers are a general way to introduce further string functions. Examples of functions that can be represented as transducers are encoders, decoders, extraction of sub-strings, removal of white-space characters, etc.

Finite-state transducers can be defined as (mutually) recursive functions, see this file for an example.

It is also possible to use prioritised finite-state transducers: multiple outgoing transitions from a state can be given priorities, and the transducer will take the transition with highest priority that will lead to a successful run. See this file for an example.

Additional regular expression constructors

Name	Explanation
re.from_ecma2020	Parse a regular expression in textual ECMAScript 2020 format (example)
re.from_ecma2020_flags	Parse a regular expression in textual ECMAScript 2020 format, with a second argument to specify flags (example)
re.case_insensitive	Make any regular expression case insensitive (example)
re.from_automaton	Parse a finite-state automaton (example)

Handling of capture groups

OSTRICH can also process regular expressions that include capture groups, lazy quantifiers, and anchors, although this is more experimental. For this functionality, OSTRICH understands a number of additional regular expression operators:

Name	Explanation
re.*?	Non-greedy star: similar to re.* but matching as few characters as possible
re.+?	Non-greedy plus
re.opt?	Non-greedy option
(_ re.loop? a b)	Non-greedy loop
(_ re.capture n)	Capture group with index n
(_ re.reference n)	Reference to the contents of capture group n
re.begin-anchor	The anchor ^
re.end-anchor	The anchor $

Such augmented regular expressions can be used in combination with several new string functions. Those functions support in particular capture groups and references in the replacement strings:

Name	Explanation
(_ str.extract n)	Extract the contents of the n'th capture group (example)
str.replace_cg	Replace the first match of a regular expression (example)
str.replace_cg_all	Replace all matches of a regular expression (example)

ostrich's People

Contributors

Stargazers

Watchers

Forkers

shlkan linusboyle amandasystems simplexiaohu matthewhague chenchengliang kurolong denis-siek

ostrich's Issues

Ostrich crashes during model extraction when there are "cyclical definitions"

Hello everyone,
I'm working on integrating Princess/Ostrich in JavaSMT to make it more easily available for Java programmers. There are a couple of issues left that are causing us some problems.

Here is the first bug I've encountered. It can be triggered like this:

import ap.theories.strings.StringTheory
import ap.SimpleAPI
import SimpleAPI.ProverStatus
import ap.parser._
import ap.theories.strings.SeqStringTheory
import ap.util.Debug
import ostrich.{OstrichStringTheory, OFlags}

import org.scalacheck.{Arbitrary, Gen, Properties}
import org.scalacheck.Prop._

object Bug1 extends Properties("Bug1") {
  Debug enableAllAssertions true

  val stringTheory = new OstrichStringTheory(List(), OFlags())

  import stringTheory._
  import IExpression._

  property("suffixPrefix") =
    SimpleAPI.withProver(enableAssert = true) { p =>
      import p._
      val a, b = createConstant(StringSort)
      !!(!((str_prefixof(a, b) & str_suffixof(b, a)) ==> (a === b)))
      ??? == ProverStatus.Unsat
    }
}

When I run the program Ostrich will crash with an "internal exception":

Running backward propagation
Warning: cyclic definitions found, ignoring some function applications
   ... disequality is not satisfied: c1 != c0
Warning: assuming -length=on to handle length constraints

Running backward propagation
Warning: cyclic definitions found, ignoring some function applications
> Exception: ap.api.SimpleAPI$SimpleAPIForwardedException: 
  Internal exception: java.lang.Exception:Model extraction failed: Right(List(0)) != Right(Vector(1))
ap.api.SimpleAPI.ap$api$SimpleAPI$$evalProverResult(SimpleAPI.scala:2150)
ap.api.SimpleAPI.ap$api$SimpleAPI$$getStatusHelp(SimpleAPI.scala:2092)
ap.api.SimpleAPI.getStatusWithDeadline(SimpleAPI.scala:2066)
ap.api.SimpleAPI.checkSatHelp(SimpleAPI.scala:1989)
ap.api.SimpleAPI.$qmark$qmark$qmark(SimpleAPI.scala:1893)

Does anybody know what could be causing this?

Assertion error on QF_S instance

Hi, for the following formula
assert_qfs.txt

ostrich 2b3eb9b

 java -jar ostrich.jar +quiet -logo +incremental QF_S.smt2
(error "Internal exception: java.lang.AssertionError: assertion failed")

Support for unsat core generation

For example below, ostrich can not generate right unsat core:

(set-option :produce-unsat-cores true)
(declare-const x String)
(declare-const i Int)
(assert (= x "hh"))
(assert (= i (str.len x)))
(assert (= i 1))

(check-sat)
(get-unsat-core)

Proving formulas with no singleton Strings

Hello
Ostrich seems to struggle with Formulas that don't contain a singleton String. Here is an example:

import ap.theories.strings.StringTheory
import ap.SimpleAPI
import SimpleAPI.ProverStatus
import ap.parser._
import ap.theories.strings.SeqStringTheory
import ap.util.Debug
import ostrich.{OstrichStringTheory, OFlags}

import org.scalacheck.{Arbitrary, Gen, Properties}
import org.scalacheck.Prop._

object Bug2 extends Properties("Bug2") {
  Debug enableAllAssertions true

  val stringTheory = new OstrichStringTheory(List(), OFlags())
  import stringTheory._
  import IExpression._

  property("lessThan") =
    SimpleAPI.withProver(enableAssert = true) { p =>
      import p._
      val a, b = createConstant(StringSort)
      !!(str_<=(a,b))
      ??? == ProverStatus.Sat
    }
}

When I run the progam Ostrich will throw an exception:

Exception: ap.api.SimpleAPI$SimpleAPIForwardedException: Internal exception: java.lang.Exception:
Cannot handle literal str_<=(c0, c1)

Is this the intended behavior, or am I doing something wrong here?

The program does work just fine when one of the arguments tostr.<= is replaced with a singleton String. Would it be possible to add support for arguments that are not singleton Strings? Or is this just one of the limitations of the algorithm that is being used?

Underscore in regex pattern causes parse error

Minimal failing example (online version):

(declare-const w String)
(assert (str.in.re w (re.from_ecma2020 '_')))
(check-sat)

Refutation unsoundness on QF_S formula with str.substr

[611] % z3release small.smt2
sat
[612] % cvc4 -q --strings-exp small.smt2
sat
[613] % ostrich +quiet small.smt2
unsat
[614] % cat small.smt2
(declare-fun a () String)
(assert (= (str.len (str.substr a 1 (str.len a))) 1))
(check-sat)
[615] %

Commit: 1b8c803

Inconsistent behavior in scala 2.13

(declare-fun y () String)

(assert (str.in.re (str.replaceall y ">" "&gt;") (re.from_ecma2020 "a")))

(check-sat)
(get-model)

The constraint above is unsat in branch scala-2.13, and sat in the master branch.

AssertionError at ReduceWithAC.scala:287

Hi, for the following QF_LRA instance
287.txt

ostrich 2b3eb9b

unsat
error
assertion failed
java.lang.AssertionError: assertion failed
        at scala.Predef$.assert(Predef.scala:156)
        at ap.terfor.arithconj.ReduceWithAC.reduceAndAdd(ReduceWithAC.scala:287)
        at ap.terfor.conjunctions.ReduceWithConjunction.ap$terfor$conjunctions$ReduceWithConjunction$$reduce(ReduceWithConjunction.scala:572)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:80)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:165)
        at ap.terfor.conjunctions.ReduceWithConjunction$$anonfun$1.apply(ReduceWithConjunction.scala:174)
        at ap.terfor.conjunctions.ReduceWithConjunction$$anonfun$1.apply(ReduceWithConjunction.scala:173)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.Iterator$class.foreach(Iterator.scala:893)
        at scala.collection.AbstractIterator.foreach(Iterator.scala:1336)
        at scala.collection.IterableLike$class.foreach(IterableLike.scala:72)
        at ap.terfor.conjunctions.NegatedConjunctions.foreach(NegatedConjunctions.scala:72)
        at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
        at ap.terfor.conjunctions.NegatedConjunctions.map(NegatedConjunctions.scala:72)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceNegatedConjs(ReduceWithConjunction.scala:173)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:99)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:165)
        at ap.terfor.conjunctions.ReduceWithConjunction$$anonfun$1.apply(ReduceWithConjunction.scala:174)
        at ap.terfor.conjunctions.ReduceWithConjunction$$anonfun$1.apply(ReduceWithConjunction.scala:173)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.Iterator$class.foreach(Iterator.scala:893)
        at scala.collection.AbstractIterator.foreach(Iterator.scala:1336)
        at scala.collection.IterableLike$class.foreach(IterableLike.scala:72)
        at ap.terfor.conjunctions.NegatedConjunctions.foreach(NegatedConjunctions.scala:72)
        at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
        at ap.terfor.conjunctions.NegatedConjunctions.map(NegatedConjunctions.scala:72)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceNegatedConjs(ReduceWithConjunction.scala:173)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:99)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:115)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:165)
        at ap.terfor.conjunctions.ReduceWithConjunction$$anonfun$1.apply(ReduceWithConjunction.scala:174)
        at ap.terfor.conjunctions.ReduceWithConjunction$$anonfun$1.apply(ReduceWithConjunction.scala:173)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.Iterator$class.foreach(Iterator.scala:893)
        at scala.collection.AbstractIterator.foreach(Iterator.scala:1336)
        at scala.collection.IterableLike$class.foreach(IterableLike.scala:72)
        at ap.terfor.conjunctions.NegatedConjunctions.foreach(NegatedConjunctions.scala:72)
        at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
        at ap.terfor.conjunctions.NegatedConjunctions.map(NegatedConjunctions.scala:72)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceNegatedConjs(ReduceWithConjunction.scala:173)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:99)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:165)
....

move ecma2020-regex-paser to repo uuverifiers

I want to use Metal or Intellij IDEA to hack the imported packages of ostrich. But the package ecma2020-regex-parser is outside of sbt repo, making me trouble to navigate to its defination.

I wish you to support the follow:

 libraryDependencies   += "uuverifiers" % "ecma2020-regex-parser" % "1.0",

AssertionError at ReduceWithConjunction.scala:424

Hi, for the following QF_LIA instance
424.txt

ostrich 2b3eb9b

error
 java.lang.AssertionError: assertion failed
        at scala.Predef$.assert(Predef.scala:156)
        at ap.terfor.conjunctions.ReduceWithConjunction.apply(ReduceWithConjunction.scala:424)
        at ap.terfor.conjunctions.ReduceWithConjunction.apply(ReduceWithConjunction.scala:413)
        at ap.SimpleAPI.flushTodo(SimpleAPI.scala:4057)
        at ap.SimpleAPI.setPartitionNumberHelp(SimpleAPI.scala:2383)
        at ap.SimpleAPI.withPartitionNumber(SimpleAPI.scala:2397)
        at ap.SimpleAPI.abbrevHelp(SimpleAPI.scala:1680)
        at ap.SimpleAPI.abbrev(SimpleAPI.scala:1663)
        at ap.SimpleAPI.abbrev(SimpleAPI.scala:1639)
        at ap.parser.SMTParser2InputAbsy$$anonfun$translateLet$8.apply(SMTParser2InputAbsy.scala:2061)
        at ap.parser.SMTParser2InputAbsy$$anonfun$translateLet$8.apply(SMTParser2InputAbsy.scala:2051)
        at scala.collection.TraversableLike$WithFilter$$anonfun$foreach$1.apply(TraversableLike.scala:733)
        at scala.collection.mutable.ResizableArray$class.foreach(ResizableArray.scala:59)
        at scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:48)
        at scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:732)
        at ap.parser.SMTParser2InputAbsy.translateLet(SMTParser2InputAbsy.scala:2051)
        at ap.parser.SMTParser2InputAbsy.translateTerm(SMTParser2InputAbsy.scala:1909)
        at ap.parser.SMTParser2InputAbsy.translateLet(SMTParser2InputAbsy.scala:2091)
        at ap.parser.SMTParser2InputAbsy.translateTerm(SMTParser2InputAbsy.scala:1909)
        at ap.parser.SMTParser2InputAbsy.translateLet(SMTParser2InputAbsy.scala:2091)
....

Solution soundness issue on QF_AUFLIA formula

Hi, for the following formula
ostrich 2b3eb9b gives sat, but z3 and cvc4 return unsat.

(set-logic QF_AUFLIA)
(declare-fun a () (Array Int Int))
(declare-fun b () (Array Int Int))
(declare-fun v () Int)
(declare-fun w () Int)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun g ((Array Int Int)) Int)
(declare-fun f (Int) Int)
(assert (and (= (store a x v) b) (= (store a y w) b) (not (= (f x) (f y))) (not (= (g a) (g b)))))
(check-sat)

Refutation soundness issue on LIRA formula

Hi, for the following instance,
ostrich 2b3eb9b yields unsat,
but z3 and cvc4 return sat

(declare-const v0 Bool)
(declare-const i1 Int)
(declare-const i4 Int)
(declare-const i5 Int)
(declare-const r0 Real)
(declare-const r2 Real)
(declare-const r3 Real)
(declare-const r7 Real)
(declare-const r9 Real)
(declare-const r10 Real)
(declare-const v1 Bool)
(declare-const i11 Int)
(assert (exists ((q0 Real) (q1 Int) (q2 Bool)) (and (> 6188.141477 r10) (= q2 q2 q2 v0 q2 q2 (> r7 3046306.76 6188.141477 153479756.0 r3) v1 v1 q2 q2) (<= i5 50))))
(assert (or (exists ((q0 Real) (q1 Int) (q2 Bool)) (=> (= 6188.141477 r0 6188.141477) (> 50 q1))) (exists ((q0 Real) (q1 Int) (q2 Bool)) v0)))
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const r12 Real)
(declare-const v4 Bool)
(declare-const r13 Real)
(assert (exists ((q3 Bool) (q4 Int) (q5 Bool) (q6 Int)) (>= 72 72)))
(declare-const v5 Bool)
(declare-const r14 Real)
(declare-const i12 Int)
(declare-const v6 Bool)
(declare-const i13 Int)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const r15 Real)
(assert (not (forall ((q7 Real) (q8 Real) (q9 Real)) (not (< 6.0 q9)))))
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const i14 Int)
(declare-const r16 Real)
(declare-const r17 Real)
(declare-const v12 Bool)
(declare-const r18 Real)
(declare-const r19 Real)
(declare-const v13 Bool)
(declare-const r20 Real)
(declare-const r21 Real)
(declare-const r22 Real)
(declare-const r23 Real)
(declare-const r24 Real)
(declare-const r25 Real)
(declare-const r26 Real)
(declare-const r27 Real)
(assert (not (forall ((q10 Real) (q11 Bool) (q12 Bool) (q13 Bool)) (not (not (> 33 (abs (to_int (* 3046306.76 90232.0 (- r0 (to_real i4) 90232.0 r12)))) 314 165 (to_int (/ r7 3046306.76))))))))
(assert (or (= (/ r7 3046306.76) 6.0) false))
(assert (or (= (/ r7 3046306.76) 6.0) false))
(assert (or (>= 72 72) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) (>= 72 72) false))
(assert (or (= (/ r7 3046306.76) 6.0) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) false))
(assert (or (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) (>= 72 72) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) (= (/ r7 3046306.76) 6.0) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) false))
(assert (or (>= 72 72) false))
(assert (or (= (/ r7 3046306.76) 6.0) (= (/ r7 3046306.76) 6.0) false))
(assert (or (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (= (/ r7 3046306.76) 6.0) (= (/ r7 3046306.76) 6.0) (= (/ r7 3046306.76) 6.0) false))
(assert (or (= (/ r7 3046306.76) 6.0) (= (/ r7 3046306.76) 6.0) false))
(assert (or (>= 72 72) (>= 72 72) (>= 72 72) false))
(assert (or (>= 72 72) false))
(assert (or (= (/ r7 3046306.76) 6.0) false))
(assert (or (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) false))
(assert (or (>= 72 72) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) (= (/ r7 3046306.76) 6.0) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) (>= 72 72) (>= 72 72) (= (/ r7 3046306.76) 6.0) false))
(assert (or (= (/ r7 3046306.76) 6.0) (= (/ r7 3046306.76) 6.0) (>= 72 72) (>= 72 72) (= (/ r7 3046306.76) 6.0) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (= (/ r7 3046306.76) 6.0) (= (/ r7 3046306.76) 6.0) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) false))
(assert (or (>= 72 72) (= (/ r7 3046306.76) 6.0) (= (/ r7 3046306.76) 6.0) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) false))
(assert (or (= (/ r7 3046306.76) 6.0) (>= 72 72) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) false))
(assert (or (>= 72 72) false))
(assert (or (= (/ r7 3046306.76) 6.0) false))
(assert (or (>= 72 72) (= (/ r7 3046306.76) 6.0) false))
(assert (or (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) (>= 72 72) (= (/ r7 3046306.76) 6.0) false))
(assert (or (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) false))
(assert (or (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (= (/ r7 3046306.76) 6.0) (= (/ r7 3046306.76) 6.0) (= (/ r7 3046306.76) 6.0) false))
(assert (or (>= 72 72) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (= (/ r7 3046306.76) 6.0) false))
(assert (or (>= 72 72) (>= 72 72) false))
(assert (or (= (/ r7 3046306.76) 6.0) false))
(assert (or (>= 72 72) (>= 72 72) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) false))
(assert (or (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) false))
(check-sat)

java.lang.RuntimeException: Stack empty

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)

Refutation soundness issue on QF_SLIA formula

Hi, for the following instance

(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const i2 Int)
(declare-const i5 Int)
(declare-const i6 Int)
(declare-const i9 Int)
(declare-const i10 Int)
(declare-const i11 Int)
(declare-const Str0 String)
(declare-const Str1 String)
(declare-const Str2 String)
(declare-const Str3 String)
(declare-const Str4 String)
(declare-const Str5 String)
(declare-const Str9 String)
(declare-const Str10 String)
(declare-const Str11 String)
(declare-const Str12 String)
(declare-const Str14 String)
(declare-const Str16 String)
(declare-const Str17 String)
(push 1)
(declare-const v4 Bool)
(declare-const i12 Int)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const i13 Int)
(declare-const i14 Int)
(declare-const v7 Bool)
(assert (>= (str.len Str14) 39))
(push 1)
(declare-const v8 Bool)
(declare-const v9 Bool)
(push 1)
(push 1)
(assert (>= (str.len (str.++ Str16 "bqlmww" Str17 Str9)) 31))
(assert (>= (str.len Str5) i5))
(declare-const v22 Bool)
(push 1)
(assert (>= (str.len (str.substr (str.++ Str1 "akkoco" "ambeqq") 0 19)) (mod (+ i5 i2 56 74) 307)))
(push 1)
(assert (>= (str.len Str3) (mod (mod (+ i5 i2 56 74) 0) 0)))
(push 1)
(assert (or (or (<= (- i10 25 i10) i13) (<= (- i10 25 i10) i13) (<= (- i10 25 i10) i13)) false))
(assert (or (or (<= (- i10 25 i10) i13) (<= (- i10 25 i10) i13) (<= (- i10 25 i10) i13)) false))
(check-sat)

ostrich 2b3eb9b returns unsat,
But both z3 and CVC4 return sat

Incorrect encoding of str.replacere

The following problem should be sat, but OSTRICH reports unsat:

(set-logic QF_S)
(declare-const w String)

; (assert (= (str.replace w "a" "") "a")) ; this works

(assert (= (str.replacere w (str.to.re "a") "") "a")) ; this does not work

(check-sat)

Solution soundness issue on AUFNIRA instance

Hi, for the following instance

(set-logic AUFNIRA)
(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 v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const i0 Int)
(declare-sort S0 0)
(assert (not (exists ((q0 Bool) (q1 S0) (q2 Int) (q3 S0) (q4 Bool) (q5 Bool)) (=> (>= q2 1) (= q3 q3)))))
(declare-const v16 Bool)
(assert (forall ((q6 (Array Int S0))) v12))
(assert v14)
(assert (forall ((q7 (Array S0 Int)) (q8 S0) (q9 S0) (q10 (Array Int S0))) (distinct (= q8 q8 q9 q8 q9) (= q10 q10 q10 q10 q10) (= q7 q7 q7 q7))))
(declare-const v17 Bool)
(assert v9)
(assert v17) 
(assert v1)
(push 1)
(assert v13)
(check-sat)

ostrich 2b3eb9b returns sat, but both z3 and cvc4 (latest commits) return unsat.

NullPointerException at SimpleAPI.scala:4116

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)

QF_S solution soundness bug with str.++

[538] % z3release small.smt2
unsat
[539] % cvc4 -q --strings-exp small.smt2
unsat
[540] % ostrich +quiet small.smt2
sat
[541] % 
[541] % cat small.smt2
(declare-fun a () String)
(assert (not (= (str.++ (str.++ a a) "A") (str.++ a (str.++ a "A")))))
(check-sat)
[542] %

[548] % z3release small.smt2
unsat
[549] % cvc4 -q --strings-exp small.smt2
unsat
[550] % ostrich +quiet small.smt2
sat
[551] % 
[551] % cat small.smt2
(declare-fun a () String)
(assert (not (= a (str.++ a ""))))
(check-sat)
[552] %

Commit: 2f3ea5c

str.<= is not reflexiv

Hello,
str.<= in Ostrich does not work quite as I expected. Here is an example program:

import ap.theories.strings.StringTheory
import ap.SimpleAPI
import SimpleAPI.ProverStatus
import ap.parser._
import ap.theories.strings.SeqStringTheory
import ap.util.Debug
import ostrich.{OstrichStringTheory, OFlags}

import org.scalacheck.{Arbitrary, Gen, Properties}
import org.scalacheck.Prop._

object Bug3 extends Properties("Bug3") {
  Debug enableAllAssertions true

  val stringTheory = new OstrichStringTheory(List(), OFlags())
  import stringTheory._
  import IExpression._

  property("lessThan") =
    SimpleAPI.withProver(enableAssert = true) { p =>
      import p._
      !!(str_<=("a", "b"))
      ??? == ProverStatus.Sat
    }

  property("lessOrEqual") =
    SimpleAPI.withProver(enableAssert = true) { p =>
      import p._
      !!(str_<=("a", "a"))
      ??? == ProverStatus.Sat
    }
}

When I run the tests, lessThan passes, but lessOrEqual fails. I was expecting them both to pass as str.<= is reflexiv in the SMT-LIB standard.

Is this an intentional change or am I just doing something wrong here?

Solution unsoundness on QF_S formula with str.substr

[598] % z3release small.smt2
unsat
[599] % cvc4 -q small.smt2
unsat
[600] % ostrich +quiet small.smt2
sat
[601] % cat small.smt2
(assert (= (str.substr "A" 0 2) ""))
(check-sat)
[602] %

Commit: 1b8c803

Compilation Error: Failed 4 out of 354 tests in Ostrich

Hello, I am facing an issue while trying to compile Ostrich. The compilation fails with the following error message:
[info] Failed: Total 354, Failed 4, Errors 0, Passed 350.
Additionally, the number of failures varies with each run.

I believe I have successfully installed sbt, as the command sbt sbtVersion outputs
[info] welcome to sbt 1.9.7 (Private Build Java 17.0.8.1).

Environment:
Operating System: Ubuntu 20.04.6 LTS

Is there any solution to this issue?
Thanks for your help!

Wrong answer of str.replace

When I try to solve the following string constraints, ostrich gives a wrong answer unsat:

(set-logic QF_S)

(declare-fun x_4 () String)
(declare-fun sigmaStar_0 () String)

(assert (= x_4 (str.replace sigmaStar_0 "ab" "c")))

(assert (str.in_re x_4 (str.to_re "aa")))

(check-sat)
(get-model)

QF_S solution soundness bug with str.at

[523] % z3release small.smt2
unsat
[524] % cvc4 -q --strings-exp small.smt2
unsat
[525] % ostrich +quiet small.smt2
sat
[526] % 
[526] % cat small.smt2
(declare-fun a () String)
(assert (not (= (str.at a 0) (str.at "" 0))))
(assert (= (str.len a) 0))
(check-sat)
[527] %

[612] % z3release small.smt2
unsat
[613] % cvc4 -q --strings-exp small.smt2
unsat
[614] % ostrich +quiet small.smt2
sat
[615] % 
[615] % cat small.smt2 
(declare-fun x () String)
(assert (distinct (str.at (str.++ "A" x) 1) (str.at x 0)))
(check-sat)
[616] %

Commit: 2f3ea5c

Assertion error at SimpleAPI.scala:3297

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)

QF_S refutation soundness bug with str.substr

[530] % z3release small.smt2
sat
[531] % cvc4 -q --strings-exp small.smt2
sat
[532] % ostrich +quiet small.smt2
unsat
[533] % 
[533] % cat small.smt2
(declare-fun a () String)
(assert (= (str.len (str.substr a 0 (- 1))) 0))
(check-sat)
[534] %

Commit: 2f3ea5c

QF_SLIA solution soundness bug with str.substr

[557] % z3release small.smt2
unsat
[558] % cvc4 -q --strings-exp small.smt2
unsat
[559] % ostrich +quiet small.smt2
sat
[560] % 
[560] % cat small.smt2
(declare-fun a () Int)
(assert (distinct (str.substr "A" 0 (+ a a)) (str.substr "A" 0 a)))
(check-sat)
[561] %

Commit: 2f3ea5c

Refutational soundness issue on QF_UFNRA formula

Hi, for the following instances
nra1.txt
nra2.txt

ostrich 2b3eb9b returns unsat, but both z3 and yices2 (latest commits) return sat .

Incorrect handling of str.replace_re

For this input, Ostrich reports unsat, cvc5 sat:

(define-fun sigmaStar_048 () String "Ajavascript:")
(define-fun b_sigmaStar_048 () Bool true)
(define-fun literal_9 () String "\u{5c}x3c\u{5c}x74\u{5c}x64\u{5c}x3e\u{5c}x55\u{5c}x52\u{5c}x4c\u{5c}x3a\u{5c}x20")
(define-fun b_literal_9 () Bool true)
(define-fun literal_11 () String "\u{5c}x3c\u{5c}x2f\u{5c}x74\u{5c}x64\u{5c}x3e")
(define-fun b_literal_11 () Bool true)
(define-fun atkPtn () String "javascript:")
(define-fun b_atkPtn () Bool false)
(define-fun x_7 () String "javascript:")
(define-fun b_x_7 () Bool true)
(define-fun x_10 () String "\u{5c}x3c\u{5c}x74\u{5c}x64\u{5c}x3e\u{5c}x55\u{5c}x52\u{5c}x4c\u{5c}x3a\u{5c}x20javascript:")
(define-fun b_x_10 () Bool true)
(define-fun x_12 () String "\u{5c}x3c\u{5c}x74\u{5c}x64\u{5c}x3e\u{5c}x55\u{5c}x52\u{5c}x4c\u{5c}x3a\u{5c}x20javascript:\u{5c}x3c\u{5c}x2f\u{5c}x74\u{5c}x64\u{5c}x3e")
(define-fun b_x_12 () Bool true)
(define-fun sink () String "\u{5c}x3c\u{5c}x74\u{5c}x64\u{5c}x3e\u{5c}x55\u{5c}x52\u{5c}x4c\u{5c}x3a\u{5c}x20javascript:\u{5c}x3c\u{5c}x2f\u{5c}x74\u{5c}x64\u{5c}x3e")
(define-fun b_sink () Bool false)
(define-fun atk_sigmaStar_1 () String "\u{5c}x3c\u{5c}x74\u{5c}x64\u{5c}x3e\u{5c}x55\u{5c}x52\u{5c}x4c\u{5c}x3a\u{5c}x20")
(define-fun atk_sigmaStar_2 () String "\u{5c}x3c\u{5c}x2f\u{5c}x74\u{5c}x64\u{5c}x3e")
(define-fun atk_sink () String "\u{5c}x3c\u{5c}x74\u{5c}x64\u{5c}x3e\u{5c}x55\u{5c}x52\u{5c}x4c\u{5c}x3a\u{5c}x20javascript:\u{5c}x3c\u{5c}x2f\u{5c}x74\u{5c}x64\u{5c}x3e")


(assert (= x_7 (str.replace_re sigmaStar_048 re.allchar "") ) )

(check-sat)

AssertionError at LinearCombination.scala:1627

Hi, for the following QF_SLIA instance
1627.txt

ostrich 2b3eb9b

error
assertion failed
java.lang.AssertionError: assertion failed
        at scala.Predef$.assert(Predef.scala:156)
        at ap.terfor.linearcombination.LinearCombination1.<init>(LinearCombination.scala:1627)
        at ap.terfor.linearcombination.LinearCombination$.apply(LinearCombination.scala:141)
        at ap.parser.InputAbsy2Internal.ap$parser$InputAbsy2Internal$$translateLinComb(InputAbsy2Internal.scala:103)
        at ap.parser.InputAbsy2Internal$$anonfun$ap$parser$InputAbsy2Internal$$translateFor$1.apply(InputAbsy2Internal.scala:115)
        at ap.parser.InputAbsy2Internal$$anonfun$ap$parser$InputAbsy2Internal$$translateFor$1.apply(InputAbsy2Internal.scala:115)
        at scala.collection.Iterator$$anon$11.next(Iterator.scala:409)
        at scala.collection.Iterator$class.foreach(Iterator.scala:893)
        at scala.collection.AbstractIterator.foreach(Iterator.scala:1336)
        at scala.collection.generic.Growable$class.$plus$plus$eq(Growable.scala:59)
        at scala.collection.mutable.ArrayBuilder$ofRef.$plus$plus$eq(ArrayBuilder.scala:99)
        at scala.collection.mutable.ArrayBuilder$ofRef.$plus$plus$eq(ArrayBuilder.scala:56)
        at ap.util.Seqs$.toArray(Seqs.scala:700)
        at ap.terfor.preds.Atom$.apply(Atom.scala:37)
        at ap.parser.InputAbsy2Internal.ap$parser$InputAbsy2Internal$$translateFor(InputAbsy2Internal.scala:114)
        at ap.parser.InputAbsy2Internal.ap$parser$InputAbsy2Internal$$translateFor(InputAbsy2Internal.scala:112)
        at ap.parser.InputAbsy2Internal.ap$parser$InputAbsy2Internal$$translateFor(InputAbsy2Internal.scala:162)
        at ap.parser.InputAbsy2Internal.ap$parser$InputAbsy2Internal$$translateFor(InputAbsy2Internal.scala:131)
        at ap.SimpleAPI.toInternal(SimpleAPI.scala:4262)
        at ap.SimpleAPI.flushTodo(SimpleAPI.scala:4044)
        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)

QF_S refutation soundness bug with str.replace

[581] % z3release small.smt2
sat
[582] % cvc4 -q --strings-exp small.smt2
sat
[583] % ostrich +quiet small.smt2
unsat
[584] % 
[584] % cat small.smt2
(declare-fun a () Bool) 
(declare-fun b () String) 
(declare-fun c () String) 
(declare-fun d () Bool) 
(declare-fun e () Bool)   
(assert (xor a e)) 
(assert (= d (not (= "" (str.replace b c (str.at b (str.len b))))))) 
(assert (= (xor a e) (= "-" c))) 
(check-sat)
[585] %

Commit: 2f3ea5c

Assertion error at SimpleAPI.scala:2283 on QF_S formula

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)

(feature) Support the new regex API names str.to_re and str.in_re

Hi,
According to http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml

The two regex operations str.to.re and str.in.re have been changed to str.to_re and str.in_re.
Is there any plan for supporting the new API names?

Refutation unsoundness on QF_S formula with str.indexof

[577] % z3release small.smt2
sat
[578] % cvc4 -q small.smt2
sat
[579] % ostrich +quiet small.smt2
unsat
[580] % cat small.smt2
(declare-fun a () String)
(assert (= (str.indexof "" "" 0) 0))
(check-sat)
[581] %

Commit: 1b8c803

Regarding Statics

How to get Statics of a model?

Refutation unsoundness on QF_S formula with str.indexof, str.substr, str.len

[622] % z3release small.smt2
sat
[623] % cvc4 -q --strings-exp small.smt2
sat
[624] % ostrich +quiet small.smt2
unsat
[625] % cat small.smt2
(declare-fun uri () String)
(assert (= (ite (= (str.indexof (str.substr uri 10 (* 125 (str.len uri) 10)) ":" 0) (- 1)) 1 0) 0))
(check-sat)
[626] %

Commit: 1b8c803

Three problems about regular expressions

Hi, I have three questions about regular expressions,

What is the difference between re. from_ecma2020 and re.from.str ?
Does OSTRICH currently support regular expressions with backreferences? E.g., (.)\1.
I found that (?=a).|c -> (model (define-fun w () String "a")), but ((?=a).|c) -> (model (define-fun w () String "\u{0}")), but \u0000 is not accepted by ((?=a).|c).

API

Does Ostrich supports JAVA API or any API's???

Miss some model

Variables without constraints do not generate model. Like the example below, the model of len_x and y will not be generated:

; sat
(declare-fun x ()String)
(declare-fun y ()String)

(declare-const len_x Int)
(declare-const len_y Int)

(assert (= len_x (str.len x)))
(assert (< 1 len_x))


(check-sat)
(get-model)

The result is:

Running backward propagation
   ... sat
(model
  (define-fun len_x () Int 2)
  (define-fun x () String "\u{0}\u{0}")
)

support scala 2.13.10

Hello! The code is not compatible with scala 2.13.10. Have you considered upgrading it to facilitate the integration of ostrich into other systems?

AssertionError at ReduceWithEqs.scala:340

Hi, for the following QF_LIA instance

340.txt

ostrich 2b3eb9b

error
 java.lang.AssertionError: assertion failed
        at scala.Predef$.assert(Predef.scala:156)
        at ap.terfor.equations.ReduceWithEqs.apply(ReduceWithEqs.scala:340)
        at ap.terfor.arithconj.ReduceWithAC.reduce(ReduceWithAC.scala:203)
        at ap.terfor.arithconj.ReduceWithAC.ap$terfor$arithconj$ReduceWithAC$$reduce(ReduceWithAC.scala:188)
        at ap.terfor.arithconj.ReduceWithAC$.ap$terfor$arithconj$ReduceWithAC$$reduceAC(ReduceWithAC.scala:70)
        at ap.terfor.arithconj.ReduceWithAC.reduceAndAdd(ReduceWithAC.scala:283)
        at ap.terfor.conjunctions.ReduceWithConjunction.ap$terfor$conjunctions$ReduceWithConjunction$$reduce(ReduceWithConjunction.scala:572)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:80)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:165)
        at ap.terfor.conjunctions.ReduceWithConjunction$$anonfun$1.apply(ReduceWithConjunction.scala:174)
        at ap.terfor.conjunctions.ReduceWithConjunction$$anonfun$1.apply(ReduceWithConjunction.scala:173)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.Iterator$class.foreach(Iterator.scala:893)
        at scala.collection.AbstractIterator.foreach(Iterator.scala:1336)
        at scala.collection.IterableLike$class.foreach(IterableLike.scala:72)
        at ap.terfor.conjunctions.NegatedConjunctions.foreach(NegatedConjunctions.scala:72)
        at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
        at ap.terfor.conjunctions.NegatedConjunctions.map(NegatedConjunctions.scala:72)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceNegatedConjs(ReduceWithConjunction.scala:173)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:99)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:165)
        at ap.terfor.conjunctions.ReduceWithConjunction$$anonfun$1.apply(ReduceWithConjunction.scala:174)
        at ap.terfor.conjunctions.ReduceWithConjunction$$anonfun$1.apply(ReduceWithConjunction.scala:173)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.Iterator$class.foreach(Iterator.scala:893)
        at scala.collection.AbstractIterator.foreach(Iterator.scala:1336)
        at scala.collection.IterableLike$class.foreach(IterableLike.scala:72)
        at ap.terfor.conjunctions.NegatedConjunctions.foreach(NegatedConjunctions.scala:72)
        at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
        at ap.terfor.conjunctions.NegatedConjunctions.map(NegatedConjunctions.scala:72)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceNegatedConjs(ReduceWithConjunction.scala:173)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:99)
        at ap.terfor.conjunctions.ReduceWithConjunction$.ap$terfor$conjunctions$ReduceWithConjunction$$reduceConj(ReduceWithConjunction.scala:165)

Assertion error at FunctionEncoder.scala:326

Hi, for the following formula
326.zip

ostrich 2b3eb9b

java.lang.AssertionError: assertion failed                                           
        at scala.Predef$.assert(Predef.scala:156)                                    
        at ap.parser.FunctionEncoder.apply(FunctionEncoder.scala:326)                 
        at ap.parser.Preprocessing$.ap$parser$Preprocessing$$encodeFunctions$1(Preprocessing.scala:106)
        at ap.parser.Preprocessing$$anonfun$27.apply(Preprocessing.scala:263)         
        at ap.parser.Preprocessing$$anonfun$27.apply(Preprocessing.scala:262)        
        at scala.collection.TraversableLike$WithFilter$$anonfun$map$2.apply(TraversableLike.scala:683)
        at scala.collection.immutable.List.foreach(List.scala:392)                   
        at scala.collection.TraversableLike$WithFilter.map(TraversableLike.scala:682) 
        at ap.parser.Preprocessing$.apply(Preprocessing.scala:262)                   
        at ap.SimpleAPI.toInternal(SimpleAPI.scala:4254)                              
        at ap.SimpleAPI.flushTodo(SimpleAPI.scala:4044)                              
        at ap.SimpleAPI.setPartitionNumberHelp(SimpleAPI.scala:2383)                  
        at ap.SimpleAPI.withPartitionNumber(SimpleAPI.scala:2397)
        at ap.SimpleAPI.abbrevHelp(SimpleAPI.scala:1680)
        at ap.SimpleAPI.abbrev(SimpleAPI.scala:1663)
        at ap.SimpleAPI.abbrev(SimpleAPI.scala:1639)
        at ap.parser.SMTParser2InputAbsy$$anonfun$translateLet$8.apply(SMTParser2InputAbsy.scala:2061)
        at ap.parser.SMTParser2InputAbsy$$anonfun$translateLet$8.apply(SMTParser2InputAbsy.scala:2051)
        at scala.collection.TraversableLike$WithFilter$$anonfun$foreach$1.apply(TraversableLike.scala:733)
        at scala.collection.mutable.ResizableArray$class.foreach(ResizableArray.scala:59)
        at scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:48)
        at scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:732)
        at ap.parser.SMTParser2InputAbsy.translateLet(SMTParser2InputAbsy.scala:2051)
       at ap.parser.SMTParser2InputAbsy$$anonfun$symApp$1.apply(SMTParser2InputAbsy.scala:2123)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.mutable.ResizableArray$class.foreach(ResizableArray.scala:59)
        at scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:48)
        at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
        at scala.collection.AbstractTraversable.map(Traversable.scala:104)
        at ap.parser.SMTParser2InputAbsy.symApp(SMTParser2InputAbsy.scala:2123)
        at ap.parser.SMTParser2InputAbsy.translateTerm(SMTParser2InputAbsy.scala:1855)
        at ap.parser.SMTParser2InputAbsy.ap$parser$SMTParser2InputAbsy$$apply(SMTParser2InputAbsy.scala:1463)
        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)

.

Assembly produces broken JAR file on case-insensitive file systems due to overlapping class names in ECMA 2020 parser

Hello, I ran the following command,
./ostrich tests/case-insensitive-2.smt2

but I got an unexpected result. Why?
(error "ecma2020regex/Absyn/ControlLettera")

Did I do something wrong?

AssertionError on UFLIA instance

Hi, for the following instance

(set-logic UFLIA) 
(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 v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const i4 Int)
(declare-const i5 Int)
(declare-const i6 Int)
(declare-const i8 Int)
(push 1)
(assert (not (exists ((q0 Bool) (q1 Bool) (q2 Bool) (q3 Bool)) (not (xor q0 q1 q0 v7 q3 v5 q2 v11 v6 v11)))))
(check-sat)
(push 1)
(declare-const v17 Bool)
(assert (exists ((q4 Bool) (q5 Bool) (q6 Int) (q7 Int)) (not (distinct v11 q5 q5 v3 q5 q4))))
(assert (or (forall ((q4 Bool) (q5 Bool) (q6 Int) (q7 Int)) v3) (exists ((q4 Bool) (q5 Bool) (q6 Int) (q7 Int)) (=> (>= q6 q6) (not q4)))))
(assert (= v9 v4 v3 v11 v1 v13 v16 v16 v2 v13))
(pop 1)
(assert (exists ((q8 Bool) (q9 Bool)) (not (=> q9 q8))))
(assert (or (exists ((q8 Bool) (q9 Bool)) (not (= v14 v6 q8 v16 q9 v10 q8 q9 (<= 45 65 4) q9))) (exists ((q8 Bool) (q9 Bool)) (<= 45 65 4))))
(assert (= v7 v7 v13 v1 v2 v2 v5 v9 v16 v12))
(check-sat)

ostrich 2b3eb9b

 java -jar ostrich.jar +assert -logo +incremental +quiet fname.smt2
unsat
(error "Internal exception: java.lang.AssertionError: assertion failed")

QF_S solution soundness bug with str.replace_all

[567] % z3release small.smt2
unsat
[568] % cvc4 -q --strings-exp small.smt2
unsat
[569] % ostrich +quiet small.smt2
sat
[570] % 
[570] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(assert (distinct (str.replace_all a "B" (str.replace_all "A" "B" b)) (str.replace_all a "B" "A")))
(check-sat)
[571] %

Commit: 2f3ea5c

Assertion error at SimpleAPI.scala:4231

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)

Potential soundness issue of unicode string encoding

Hi, for the following formula

(set-logic QF_S)
(assert (= "\x4a" "\x4A"))
(check-sat)

ostrich and z3 yield sat,
but cvc4 gives unsat.

Intuitively, I may respect the result would be unsat.
Is this different because of the changes in the SMT-LIB2 standard?

uuverifiers / ostrich Goto Github PK

ostrich's Introduction

OSTRICH

An SMT Solver for String Constraints

Using Ostrich

Web Interface

Input Format

Additional string functions

Unary transducers

Additional regular expression constructors

Handling of capture groups

ostrich's People

Contributors

Stargazers

Watchers

Forkers

ostrich's Issues

Recommend Projects

Recommend Topics

Recommend Org