z3py: why does the check time vary so much after renaming the variable?

Question

I observed that the check time of my logical formulas written in z3py changed a lot (from ~60s to ~30s, about 50%) after I removed "-" in the names of the variables that I defined.

E.g.,

vec = IntVector('vec-1',10)

to

vec = IntVector('vec1',10)

Is this something expected? If so, why?

Probably, one of those forms has a name collision. In that case Z3 references the same constant twice instead of throwing an error. So you are solving a different formula. — usr, Sep 19 '15 at 20:36

score 2 · Answer 1 · answered Sep 20 '15 at 09:48

2

Probably, one of those forms has a name collision. In that case Z3 references the same constant twice instead of throwing an error. So you are solving a different formula.

answered Sep 20 '15 at 09:48

usr

165,323
34
234
359

That sounds interesting. Could you please provide an example (SMTLib or Z3Py) that illustrates the problem? – Malte Schwerhoff Sep 23 '15 at 08:18
I can try to synthesize one. – Zhongjun 'Mark' Jin Sep 24 '15 at 14:33
I think this ticket explained the reason http://stackoverflow.com/questions/15619592/z3-timing-variation/15627388#15627388 – Zhongjun 'Mark' Jin Oct 09 '15 at 20:25
@Zhongjun'Mark'Jin Nice! Thank you – Malte Schwerhoff Oct 13 '15 at 14:55

z3py: why does the check time vary so much after renaming the variable?

1 Answers1