Update cardinality in strings to unicode standard (#4402)

This updates the default cardinality in strings to match the Unicode standard, 196608.

This avoids a check-model failure from 25 benchmarks in SMT-LIB, which were related to a split due to insufficient constants being required during collectModelInfo.

This also makes a few places throw an AlwaysAssert(false) that otherwise would lead to incorrect models. These regardless should never throw, but it would be better to have an assertion failure.

1 files changed, 12 insertions, 0 deletions

diff --git a/test/regress/regress2/strings/cmi-split-cm-fail.smt2 b/test/regress/regress2/strings/cmi-split-cm-fail.smt2
new file mode 100644
index 000000000..e2ae94a27
--- /dev/null
+++ b/test/regress/regress2/strings/cmi-split-cm-fail.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --strings-exp --rewrite-divk
+; EXPECT: sat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_SLIA)
+(set-info :status sat)
+
+(declare-fun s () String)
+
+(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (not (= (ite (not (= (str.at s 0) (str.at s 1))) 1 0) 0)))) (not (= (ite (not (= (str.at s 3) (str.at s 5))) 1 0) 0))) (not (not (= (ite (not (= (str.at s 2) (str.at s 6))) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 1) (str.at s 7))) 1 0) 0)))) (not (= (ite (not (= (str.at s 2) (str.at s 5))) 1 0) 0))) (not (not (= (ite (not (= (str.at s 1) (str.at s 6))) 1 0) 0)))) (not (= (ite (not (= (str.at s 1) (str.at s 5))) 1 0) 0))) (not (= (ite (not (= (str.at s 1) (str.at s 4))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 4) (str.at s 5))) 1 0) 0)))) (not (= (ite (not (= (str.at s 5) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 5) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 1) (str.at s 3))) 1 0) 0)))) (not (= (ite (not (= (str.at s 4) (str.at s 6))) 1 0) 0))) (not (not (= (ite (not (= (str.at s 3) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 4) (str.at s 5))) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 3) (str.at s 6))) 1 0) 0)))) (not (= (ite (not (= (str.at s 3) (str.at s 5))) 1 0) 0))) (not (= (ite (not (= (str.at s 3) (str.at s 4))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 4) (str.at s 5))) 1 0) 0)))) (not (= (ite (not (= (str.at s 5) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 5) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 3) 1 0) 0)))) (not (not (= (ite (= (str.len s) 3) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 1) (str.at s 2))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 4) (str.at s 5))) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 3) (str.at s 6))) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 2) (str.at s 7))) 1 0) 0)))) (not (= (ite (not (= (str.at s 3) (str.at s 5))) 1 0) 0))) (not (not (= (ite (not (= (str.at s 2) (str.at s 6))) 1 0) 0)))) (not (= (ite (not (= (str.at s 2) (str.at s 5))) 1 0) 0))) (not (= (ite (not (= (str.at s 2) (str.at s 4))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 4) (str.at s 5))) 1 0) 0)))) (not (= (ite (not (= (str.at s 5) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 5) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 2) (str.at s 3))) 1 0) 0)))) (not (= (ite (not (= (str.at s 4) (str.at s 6))) 1 0) 0))) (not (not (= (ite (not (= (str.at s 3) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 4) (str.at s 5))) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 3) (str.at s 6))) 1 0) 0)))) (not (= (ite (not (= (str.at s 3) (str.at s 5))) 1 0) 0))) (not (= (ite (not (= (str.at s 3) (str.at s 4))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 4) (str.at s 5))) 1 0) 0)))) (not (= (ite (not (= (str.at s 5) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 5) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 3) 1 0) 0)))) (not (not (= (ite (= (str.len s) 3) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 2) 1 0) 0)))) (not (not (= (ite (= (str.len s) 2) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 1) 1 0) 0)))) (not (not (= (ite (= (str.len s) 1) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 0) 1 0) 0)))) (not (not (= (ite (= (str.len s) 0) 1 0) 0)))))
+
+(check-sat)
+(exit)