z3 hang issue: consider removing dirty timeout from z3 about nnsmith HOT 5 CLOSED

It is always frequent to get no valid range found, though we don't desire huge models at this point, which is a place demanding improvement.

from nnsmith.

Since we use sub-processes to control the timeout, why do we still need...

Without the z3 timeout, everytime z3 hangs, the generation process will timeout as well. So I set the timeout for z3 to be 3x smaller: https://github.com/ise-uiuc/nnsmith/blob/main/nnsmith/graph_gen.py#L265, allowing z3 to hang at most 3 times without making the process timeout. I didn't test to see if this does improve fail rate. If you didn't see much change (in large graph with 30 nodes or more in particular) then sure please disable it.

BTW did you confirm that unknown is really caused by timeout? That is, if without timeout, will z3 returns sat within time limit? I am having a hard time convincing myself timeout makes z3 buggy. Could you give me some reference on that?

It is always frequent to get no valid range found, though we don't desire huge models at this point, which is a place demanding improvement.

Good point, need to track this if we are going to have graphs of 30 nodes or more. On my end 30% of then give no valid range found for 30-node graph. Let me open a new issue to track.

from nnsmith.

BTW did you confirm that unknown is really caused by timeout?

@lazycal

https://github.com/Z3Prover/z3/blob/master/src/cmd_context/cmd_context.cpp#L1704

from nnsmith.

My question is

if without timeout, will z3 returns sat within time limit?

Why is the link related to that?

Or you mean the link is answering my latter question:

I am having a hard time convincing myself timeout makes z3 buggy. Could you give me some reference on that?

But I don't see the connection either. Sorry I don't know much about z3 internals.

from nnsmith.

solver.check() returns:

1. sat
2. unsat
3. unknown

See: https://stackoverflow.com/questions/11197344/z3-produces-unknown-for-assertions-without-quantifiers

timeout will give you unknown. There could be other reasons for unknown. To debug and understand why:

print( solver.statistics() )
# Traversing statistics
for k, v in solver.statistics():
    print( "%s : %s" % (k, v) )

Another things I noticed is to not use / but div. See Z3Prover/z3#756

from nnsmith.