+++
title = "Add check of correctness for Iop"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a8g5h5"]
forwardlinks = []
zettelid = "3a8g5h6"
+++

At each Iop, the defining variable should not be in the predicate. Once
the simplification is not present anymore, it will be difficult to prove
that the Iop instruction does not modify the value of the current
predicate. Because of this, the current development always removes all
the variables from the predicate that are currently being defined there.