fix reflexivity of strings

src/main/scala/ostrich/automata/BricsAutomaton.scala

@@ -241,6 +241,7 @@ object BricsAutomaton {
       builder.setAccept(states(n), isAccepting = true)
     }
 
+    builder.setAccept(states.last, isAccepting = true)
     builder.getAutomaton
   }
   /**
@@ -285,7 +286,6 @@ object BricsAutomaton {
       builder.addTransition(states(n),builder.LabelOps.singleton(c), states(n+1))
       // we read c < x -> go to sink state
       builder.addTransition(states(n),builder.LabelOps.interval((c+1).toChar, Char.MaxValue), sink_state)
-      builder.setAccept(states(n), isAccepting = true)
     }
     // we are equal up to this point -> can read any letter afterwards and be bigger
     builder.setAccept(states.last, isAccepting = true)

src/test/scala/SMTLIBTests.scala

@@ -472,8 +472,14 @@ object SMTLIBTests extends Properties("SMTLIBTests") {
     checkFile("tests/str-leq12.smt2", "sat")
   property("str-leq13") =
     checkFile("tests/str-leq13.smt2", "error")
+  property("str-leq14") =
+    checkFile("tests/str-leq14.smt2", "unsat")
   property("str-lt") =
     checkFile("tests/str-lt.smt2", "sat")
   property("str-lt2") =
     checkFile("tests/str-lt2.smt2", "unsat")
+  property("str-leq-reflexive") =
+    checkFile("tests/str-leq-reflexive.smt2", "sat")
+  property("str-leq-reflexive-2") =
+    checkFile("tests/str-leq-reflexive-2.smt2", "sat")
 }

tests/str-leq-reflexive-2.smt2

@@ -0,0 +1,5 @@
+(set-logic QF_SLIA)
+
+(assert (str.<= "abc" "abd"))
+(assert (str.<= "abc" "abc"))
+(check-sat)

tests/str-leq-reflexive.smt2

@@ -0,0 +1,5 @@
+(set-logic QF_SLIA)
+
+(assert (str.<= "a" "b"))
+(assert (str.<= "a" "a"))
+(check-sat)

tests/str-leq14.smt2

@@ -0,0 +1,6 @@
+(set-logic QF_SLIA)
+
+(declare-fun x () String)
+(assert (str.in.re x (str.to.re "a")))
+(assert (str.<= "abc" x))
+(check-sat)