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)