Performance scales unexpectedly non linear

Using powershell (on windows) I generated regular expression problems in which the minimal elements in the loop varies. I expected that the time for cvc4 to solve these problems would increase linear with the minimal elements in the loop. However, I obtained

minimal elements in loop	time (ms)
0	36,3953
1	47,4381
2	48,905
5	63,6582
10	133,5371
20	319,4708
50	2284,578
100	11657,9906
200	74854,9273

This performance seems prohibitive for real-world problems where long string are quite common.

Is the performance fundamentally non-linear? If not, could the performance be made linear?

Details:

The ps1 script to generate Problems was

param($p1)
echo "(set-info :smt-lib-version 2.5)"
echo "(set-option :produce-models true)"
echo "(set-logic ALL)"
echo "(declare-fun v0() String)"
echo "(assert (str.in.re v0 (re.loop (re.++ (re.range ""\xd5"" ""\xe0"")(re.range ""@"" ""^"")) " $p1 ")))"
echo "(check-sat)"
echo "(exit)"

The output for this generation script with 10 as parameter is

(set-info :smt-lib-version 2.5)
(set-option :produce-models true)
(set-logic ALL)
(declare-fun v0() String)
(assert (str.in.re v0 (re.loop (re.++ (re.range "\xd5" "\xe0")(re.range "@" "^"))
10
)))
(check-sat)
(exit)

The script to measure the time was (it includes a run-in measurement to incorporate caching effects)

0, 0, 1, 2, 5, 10, 20, 50, 100, 200 | 
    ForEach-Object { 
        $m = Measure-Command {
            .\genProblem.ps1 $_ | cvc4 --lang=smt2.5 --strings-exp --fmf-fun-rlv --uf-ss-fair --no-strings-print-ascii
        }
        $t = $m.TotalMilliseconds
        echo "$_ $t"
    }

cvc5 / cvc5-projects

Performance scales unexpectedly non linear #37

Details: