Open ArpitaDutta opened 1 year ago
Our solver call has timeout, there is probably an infinite loop at some point in the solver related calls.
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
Let's discuss this in next meeting
The following program is getting indefinitely stuck in the
Z3 Solver
.At some point in time, the following expression is passed from the pushup () to the z3 solver for simplification.
After applying the
txExpr2z3Expr
, the following z3 expr is obtained.Above expr is sent to
applyTactic(c, "simplify", z3e)
and the obtained simplified z3 expr is as follows:Subsequently, the above z3 expr is supplied to the
applyTactic(c, "ctx-solver-simplify", z3e)
, but, the program is getting stuck at this point.