str.<= is not reflexiv

[daniel-raffler]

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?

[daniel-raffler]

Thanks! This seems to have fixed it