1

Closed

ctx-simplify refcounting issue

description

It seems like something is wrong with reference counting in ctx_simplify_tactic::imp::m_occs. Right now, when I run the Python program here:

http://es.csail.mit.edu/z3-refcount-bug.py

I get the following output:

Or(a, And(Not(b), Not(And(Not(b), c)))) -> [[Or(a, And(Not(b), Not(And(Not(b), c))))]]

meaning, the Not(b) inside the Not(And(...)) is not getting simplified away. In principle, ctx-simplify-tactic should be getting this right, but it turns out this isn't getting simplified because ctx_simplify_tactic::imp::shared() returns false for the 'b' expression. This is despite the fact that 'b' is, infact, shared. After I apply this patch, which ignores m_occs in shared():

http://es.csail.mit.edu/0002-fix-ctx-simplify-to-properly-deal-with-this-case.patch

the simplification finally works, where the same program produces:

Or(a, And(Not(b), Not(And(Not(b), c)))) -> [[Or(a, And(Not(b), Not(c)))]]
Closed Jun 7, 2013 at 2:32 AM by leodemoura
Fixed in the unstable branch.

comments

leodemoura wrote Jun 7, 2013 at 2:32 AM

The bug was fixed in the unstable branch.
https://z3.codeplex.com/SourceControl/changeset/2b59f2ecc2b0cb7621c8558cd635a2b930b71097

The reference counter was correct. There is only one occurrence of b (as a child of Not), but there are many occurrences of Not(b). The code for handling the Not was ignoring this fact.