Indefinitely stuck in the Z3 solver

[ArpitaDutta]

The following program is getting indefinitely stuck in the Z3 Solver.

#include <klee/klee.h>
#define N 36
#define MAX 9999

int a[N+1];
int alwaystrue(int n);
int f(int n);

main() {
    int sum = 0;
    for (int i = 1; i <= N; i++) a[i] = i;
    for (int i = 1; i <= N; i++) {
        int choice;
        klee_make_symbolic(&choice, sizeof(int), "choice");
        if (choice) sum++;
        else {
            if (alwaystrue(sum + 777)) sum += 2; else sum = MAX;
        }
    }
    
    klee_assert(sum <= 2*N);
}

int alwaystrue(int n) {
    if (n*n/33 > 45) return f(n + 444);
    else return f(n + 555);
}

int f(int n) {
    int sum = 0;
    for (int i = 1; i <= N; i++) sum += a[i];
    return sum - n*(n + 1)/2 + 1;
} 

At some point in time, the following expression is passed from the pushup () to the z3 solver for simplification.

(And (And (And (Sle N0:(WPVar w32 (sum)) 70)
                (Not (Sle (WPVar w32 (i1)) 35)))
           (Not (Eq 4294967295
                    (Add w32 N0
                             (Mul w32 4294967295
                                      (SDiv w32 (Mul w32 (Add w32 1221 N0) (Add w32 1222 N0))
                                                2))))))
      (Slt 45
           (SDiv w32 (Mul w32 N1:(Add w32 777 N0) N1)
                     33)))

After applying the txExpr2z3Expr, the following z3 expr is obtained.

(let ((a!1 (* (- 1) (div (* (+ 1221 sum) (+ 1222 sum)) 2)))
      (a!2 (< 45 (div (* (+ 777 sum) (+ 777 sum)) 33))))
  (and (<= sum 70) (not (<= i1 35)) (not (= (- 1) (+ sum a!1))) a!2))

Above expr is sent to applyTactic(c, "simplify", z3e) and the obtained simplified z3 expr is as follows:

(let ((a!1 (* (- 1) (div (* (+ 1221 sum) (+ 1222 sum)) 2)))
      (a!2 (<= (div (* (+ 777 sum) (+ 777 sum)) 33) 45)))
  (and (<= sum 70) (not (<= i1 35)) (not (= (- 1) (+ sum a!1))) (not a!2)))

Subsequently, the above z3 expr is supplied to the applyTactic(c, "ctx-solver-simplify", z3e),
but, the program is getting stuck at this point.

[rasoolmaghareh]

Our solver call has timeout, there is probably an infinite loop at some point in the solver related calls.

[ArpitaDutta]

I have tried to set the solver time e.g., --max-solver-time=2 but the system is unable to recognize its effect.
-max-solver-time=<seconds> - Maximum amount of time for a single SMT query (default=0s (off)). Enables --use-forked-solver

Is there any way to come out of these?

Can I try to set the timeout for ctx-solver-simplify using this stack overflow procedure?
set timeout for Z3's ctx-solver-simplify tactic

[rasoolmaghareh]

Let's discuss this in next meeting