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:
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():
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)))]]