Log level affects Z3 behavior

[s0mark]

Running Theta in different log level configurations leads to Z3Exception for certain log levels, while resulting in successful verification for others.

Theta version: b56a6ac Input task: recursive-simple/id2_b3_o2.c Configuration: --domain PRED_CART --refinement BW_BIN_ITP --search BFS --lbe NO_LBE Platform: MacOS 10.15

Results based on log level setting:	loglevel	verification	result
RESULT	✅	unsafe
MAINSTEP	✅	unsafe
SUBSTEP	✅	unsafe
INFO	✅	unsafe
DETAIL	❌	Z3Exception
VERBOSE	❌	Z3Exception

Stack trace:

com.microsoft.z3.Z3Exception: not an inequality
    at com.microsoft.z3.Native.getInterpolant(Native.java:5468)
    at com.microsoft.z3.InterpolationContext.GetInterpolant(InterpolationContext.java:91)
    at hu.bme.mit.theta.solver.z3.Z3ItpSolver.getInterpolant(Z3ItpSolver.java:105)
    at hu.bme.mit.theta.analysis.expr.refinement.ExprTraceBwBinItpChecker.check(ExprTraceBwBinItpChecker.java:125)
    at hu.bme.mit.theta.analysis.expr.refinement.SingleExprTraceRefiner.refine(SingleExprTraceRefiner.java:94)
    at hu.bme.mit.theta.xcfa.analysis.XcfaSingleExprTraceRefiner.refine(XcfaSingeExprTraceRefiner.kt:73)
    at hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker.check(CegarChecker.java:106)
    at hu.bme.mit.theta.xcfa.cli.XcfaCegarConfig.check(XcfaCegarConfig.kt:188)
    at hu.bme.mit.theta.xcfa.cli.XcfaCli$runDirect$1.invoke(XcfaCli.kt:311)
    at hu.bme.mit.theta.xcfa.cli.XcfaCli$runDirect$1.invoke(XcfaCli.kt:311)
    at hu.bme.mit.theta.xcfa.cli.ExitCodesKt.exitOnError(ExitCodes.kt:56)
    at hu.bme.mit.theta.xcfa.cli.XcfaCli.runDirect(XcfaCli.kt:311)
    at hu.bme.mit.theta.xcfa.cli.XcfaCli.run(XcfaCli.kt:263)
    at hu.bme.mit.theta.xcfa.cli.XcfaCli.access$run(XcfaCli.kt:83)
    at hu.bme.mit.theta.xcfa.cli.XcfaCli$Companion.main(XcfaCli.kt:615)
    at hu.bme.mit.theta.xcfa.cli.XcfaCli.main(XcfaCli.kt)
Process failed! (hu.bme.mit.theta.solver.z3.Z3ItpSolver.getInterpolant(Z3ItpSolver.java:105), com.microsoft.z3.Z3Exception: not an inequality)