Fix isLeq function in String utility (#3659)

4 files changed, 270 insertions, 2 deletions

diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index d91280926..ee63308ab 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -331,11 +331,13 @@ bool String::isLeq(const String &y) const
     {
       return false;
     }
-    if (d_str[i] > y.d_str[i])
+    unsigned ci = convertUnsignedIntToCode(d_str[i]);
+    unsigned cyi = convertUnsignedIntToCode(y.d_str[i]);
+    if (ci > cyi)
     {
       return false;
     }
-    if (d_str[i] < y.d_str[i])
+    if (ci < cyi)
     {
       return true;
     }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 418670fa6..bd3665727 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -889,6 +889,7 @@ set(regress_0_tests
   regress0/strings/issue2958.smt2
   regress0/strings/issue3440.smt2
   regress0/strings/issue3497.smt2
+  regress0/strings/issue3657-evalLeq.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/leadingzero001.smt2
   regress0/strings/loop001.smt2
@@ -1653,6 +1654,7 @@ set(regress_1_tests
   regress1/strings/issue3217.smt2
   regress1/strings/issue3272.smt2
   regress1/strings/issue3357.smt2
+  regress1/strings/issue3657-unexpectedUnsatCVC4.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2
diff --git a/test/regress/regress0/strings/issue3657-evalLeq.smt2 b/test/regress/regress0/strings/issue3657-evalLeq.smt2
new file mode 100644
index 000000000..a557f4e62
--- /dev/null
+++ b/test/regress/regress0/strings/issue3657-evalLeq.smt2
@@ -0,0 +1,6 @@
+(set-info :smt-lib-version 2.5)
+(set-logic ALL)
+(set-info :status sat)
+(assert (not (str.< "\xe8" "\x19")))
+(check-sat)
+(exit)
diff --git a/test/regress/regress1/strings/issue3657-unexpectedUnsatCVC4.smt2 b/test/regress/regress1/strings/issue3657-unexpectedUnsatCVC4.smt2
new file mode 100644
index 000000000..b2bb29577
--- /dev/null
+++ b/test/regress/regress1/strings/issue3657-unexpectedUnsatCVC4.smt2
@@ -0,0 +1,258 @@
+; COMMAND-LINE: --strings-exp --fmf-fun-rlv -i

+; EXPECT: sat

+; EXPECT: sat

+; EXPECT: sat

+; EXPECT: sat

+; EXPECT: sat

+; EXPECT: sat

+; EXPECT: sat

+; EXPECT: sat

+; EXPECT: sat

+; EXPECT: sat

+; EXPECT: sat

+(set-info :smt-lib-version 2.5)

+(set-option :produce-models true)

+(set-logic ALL)

+(declare-datatypes () ((a0(c0$0)(c0$1)(c0$2)(c0$3(c0$3$0 a1)(c0$3$1 Int)(c0$3$2 String)(c0$3$3 Int))(c0$4(c0$4$0 Int))(c0$5))(a1(c1$0(c1$0$0 a0)(c1$0$1 a0)(c1$0$2 String)(c1$0$3 Int))(c1$1(c1$1$0 Int))(c1$2)(c1$3(c1$3$0 Int))(c1$4)(c1$5))(a2(c2$0(c2$0$0 Int)(c2$0$1 a0))(c2$1(c2$1$0 String)(c2$1$1 a0)(c2$1$2 a1)))))

+(push 1)

+(pop 1)

+(push 1)

+(declare-fun v0() a0)

+(declare-fun v1() a2)

+(declare-fun v2() a2)

+(declare-fun v3() a0)

+(declare-fun v4() Bool)

+(declare-fun v5() a1)

+(declare-fun v6() Bool)

+(declare-fun v7() String)

+(declare-fun v8() a2)

+(pop 1)

+(push 1)

+(pop 1)

+(push 1)

+(declare-fun v9() a2)

+(declare-fun va() a1)

+(declare-fun vb() Int)

+(declare-fun vc() Bool)

+(declare-fun vd() Int)

+(declare-fun ve() Bool)

+(declare-fun vf() Bool)

+(pop 1)

+(push 1)

+(declare-fun v10() a1)

+(declare-fun v11() a0)

+(declare-fun v12() a1)

+(declare-fun v13() Int)

+(pop 1)

+(push 1)

+(declare-fun v14() Bool)

+(declare-fun v15() a0)

+(declare-fun v16() Bool)

+(declare-fun v17() a1)

+(declare-fun v18() a2)

+(declare-fun v19() a0)

+(declare-fun v1a() Int)

+(declare-fun v1b() Bool)

+(pop 1)

+(push 1)

+(declare-fun v1c() String)

+(declare-fun v1d() Int)

+(declare-fun v1e() a1)

+(declare-fun v1f() a0)

+(declare-fun v20() Bool)

+(declare-fun v21() Int)

+(declare-fun v22() Int)

+(declare-fun v23() String)

+(declare-fun v24() a0)

+(declare-fun v25() a0)

+(pop 1)

+(push 1)

+(declare-fun v26() Bool)

+(declare-fun v27() Bool)

+(declare-fun v28() Int)

+(declare-fun v29() a2)

+(declare-fun v2a() Int)

+(declare-fun v2b() Int)

+(declare-fun v2c() String)

+(declare-fun v2d() String)

+(pop 1)

+(push 1)

+(declare-fun v2e() a2)

+(declare-fun v2f() a1)

+(declare-fun v30() a0)

+(declare-fun v31() a2)

+(declare-fun v32() String)

+(declare-fun v33() Bool)

+(declare-fun v34() Int)

+(pop 1)

+(push 1)

+(declare-fun v35() String)

+(declare-fun v36() a1)

+(declare-fun v37() a1)

+(pop 1)

+(push 1)

+(declare-fun v38() a2)

+(declare-fun v39() Bool)

+(pop 1)

+(define-funs-rec ((fa((v38 a2)(v39 Bool))a2)(f9((v35 String)(v36 a1)(v37 a1))String)(f8((v2e a2)(v2f a1)(v30 a0)(v31 a2)(v32 String)(v33 Bool)(v34 Int))a0)(f7((v26 Bool)(v27 Bool)(v28 Int)(v29 a2)(v2a Int)(v2b Int)(v2c String)(v2d String))a0)(f6((v1c String)(v1d Int)(v1e a1)(v1f a0)(v20 Bool)(v21 Int)(v22 Int)(v23 String)(v24 a0)(v25 a0))Int)(f5((v14 Bool)(v15 a0)(v16 Bool)(v17 a1)(v18 a2)(v19 a0)(v1a Int)(v1b Bool))a0)(f4((v10 a1)(v11 a0)(v12 a1)(v13 Int))Bool)(f3((v9 a2)(va a1)(vb Int)(vc Bool)(vd Int)(ve Bool)(vf Bool))Int)(f2()Int)(f1((v0 a0)(v1 a2)(v2 a2)(v3 a0)(v4 Bool)(v5 a1)(v6 Bool)(v7 String)(v8 a2))Int)(f0()Bool))(v38 "\xea" (c0$3 c1$5 1 "\xc6\xff" (- 2)) c0$5 (- 9) (c0$3 c1$4 0 "" v1a) (str.< (ite (is-c0$4 v11) "\xe8" "") "\x19") 0 (- 1) 0 false))

+(push 1)

+(assert true)

+(check-sat)

+(pop 1)

+(push 1)

+(declare-fun v3a() a0)

+(declare-fun v3b() a2)

+(declare-fun v3c() a2)

+(declare-fun v3d() a0)

+(declare-fun v3e() Bool)

+(declare-fun v3f() a1)

+(declare-fun v40() Bool)

+(declare-fun v41() String)

+(declare-fun v42() a2)

+(assert true)

+(assert (= (c0$4 0) v3a))

+(assert (= (c2$1 ";," c0$0 c1$4) v3b))

+(assert (= (c2$1 ";," c0$0 c1$4) v3c))

+(assert (= (c0$4 0) v3d))

+(assert v3e)

+(assert (= c1$2 v3f))

+(assert v40)

+(assert (= "\xc4\xbf)9N\xc2]" v41))

+(assert (= (c2$1 ";," c0$0 c1$4) v42))

+(check-sat)

+(pop 1)

+(push 1)

+(assert true)

+(check-sat)

+(pop 1)

+(push 1)

+(declare-fun v43() a2)

+(declare-fun v44() a1)

+(declare-fun v45() Int)

+(declare-fun v46() Bool)

+(declare-fun v47() Int)

+(declare-fun v48() Bool)

+(declare-fun v49() Bool)

+(assert true)

+(assert (= (c2$1 ";," c0$0 c1$4) v43))

+(assert (= c1$2 v44))

+(assert (= 9 v45))

+(assert v46)

+(assert (= 9 v47))

+(assert v48)

+(assert v49)

+(check-sat)

+(pop 1)

+(push 1)

+(declare-fun v4a() a1)

+(declare-fun v4b() a0)

+(declare-fun v4c() a1)

+(declare-fun v4d() Int)

+(assert (not (f4 v4a v4b v4c v4d)))

+(assert (= c1$2 v4a))

+(assert (= (c0$4 0) v4b))

+(assert (= c1$2 v4c))

+(assert (= 9 v4d))

+(check-sat)

+(pop 1)

+(push 1)

+(declare-fun v4e() Bool)

+(declare-fun v4f() a0)

+(declare-fun v50() Bool)

+(declare-fun v51() a1)

+(declare-fun v52() a2)

+(declare-fun v53() a0)

+(declare-fun v54() Int)

+(declare-fun v55() Bool)

+(assert (= (c0$3 c1$4 0 "" 9) (f5 v4e v4f v50 v51 v52 v53 v54 v55)))

+(assert v4e)

+(assert (= (c0$4 0) v4f))

+(assert v50)

+(assert (= c1$2 v51))

+(assert (= (c2$1 ";," c0$0 c1$4) v52))

+(assert (= (c0$4 0) v53))

+(assert (= 9 v54))

+(assert v55)

+(check-sat)

+(pop 1)

+(push 1)

+(declare-fun v56() String)

+(declare-fun v57() Int)

+(declare-fun v58() a1)

+(declare-fun v59() a0)

+(declare-fun v5a() Bool)

+(declare-fun v5b() Int)

+(declare-fun v5c() Int)

+(declare-fun v5d() String)

+(declare-fun v5e() a0)

+(declare-fun v5f() a0)

+(assert true)

+(assert (= "\xc4\xbf)9N\xc2]" v56))

+(assert (= 9 v57))

+(assert (= c1$2 v58))

+(assert (= (c0$4 0) v59))

+(assert v5a)

+(assert (= 9 v5b))

+(assert (= 9 v5c))

+(assert (= "\xc4\xbf)9N\xc2]" v5d))

+(assert (= (c0$4 0) v5e))

+(assert (= (c0$4 0) v5f))

+(check-sat)

+(pop 1)

+(push 1)

+(declare-fun v60() Bool)

+(declare-fun v61() Bool)

+(declare-fun v62() Int)

+(declare-fun v63() a2)

+(declare-fun v64() Int)

+(declare-fun v65() Int)

+(declare-fun v66() String)

+(declare-fun v67() String)

+(assert true)

+(assert v60)

+(assert v61)

+(assert (= 9 v62))

+(assert (= (c2$1 ";," c0$0 c1$4) v63))

+(assert (= 9 v64))

+(assert (= 9 v65))

+(assert (= "\xc4\xbf)9N\xc2]" v66))

+(assert (= "\xc4\xbf)9N\xc2]" v67))

+(check-sat)

+(pop 1)

+(push 1)

+(declare-fun v68() a2)

+(declare-fun v69() a1)

+(declare-fun v6a() a0)

+(declare-fun v6b() a2)

+(declare-fun v6c() String)

+(declare-fun v6d() Bool)

+(declare-fun v6e() Int)

+(assert true)

+(assert (= (c2$1 ";," c0$0 c1$4) v68))

+(assert (= c1$2 v69))

+(assert (= (c0$4 0) v6a))

+(assert (= (c2$1 ";," c0$0 c1$4) v6b))

+(assert (= "\xc4\xbf)9N\xc2]" v6c))

+(assert v6d)

+(assert (= 9 v6e))

+(check-sat)

+(pop 1)

+(push 1)

+(declare-fun v6f() String)

+(declare-fun v70() a1)

+(declare-fun v71() a1)

+(assert true)

+(assert (= "\xc4\xbf)9N\xc2]" v6f))

+(assert (= c1$2 v70))

+(assert (= c1$2 v71))

+(check-sat)

+(pop 1)

+(push 1)

+(declare-fun v72() a2)

+(declare-fun v73() Bool)

+(assert (= (c2$1 ";," c0$0 c1$4) (fa v72 v73)))

+(assert (= (c2$1 ";," c0$0 c1$4) v72))

+(assert v73)

+(check-sat)

+(pop 1)

+(exit)