# Hardware Model Checking Algorithms and Techniques
## 6 Ic3
It is in fact possible for an enqueued proof obligation to become discharged as a result of some previous proof-obligation discharging. To perform this check, the algorithm tests whether \(q\) is still included in \(F_{j}\) (line 5). This can be performed by posing the following SAT query:  
\[SAT(F_{j}\wedge q) \tag{58}\]  
If \(q\) is in \(F_{j}\) (i.e., Query (58) is SAT), the proof obligation \((q,j)\) still needs to be discharged. Otherwise, \(q\) has already been blocked in \(F_{j}\) and the procedure can move on to the next iteration. If the proof obligation \((q,j)\) still needs to be discharged, then IC3 checks whether \(F_{j}\) is the initial frame (line 6). If so, the states represented by \(q\) are initial states that can reach a violation of property \(P\). Thus, a counterexample to \(P\) can be constructed by following the chain of proof obligations that led to \((q,0)\). This is performed by means of the procedure ReconstructCex(\(q\)), not described here. In that case, the procedure terminates with a failure and returns the counterexample found. To discharge a proof obligation \((q,j)\), i.e., to block a cube \(q\) in \(F_{j}\), IC3 tries to derive a clause \(c\) such that \(c\subseteq\
eg q\) and \(c\) is inductive relative to \(F_{j-1}\). Figure (b)b visualizes this step. The _initiation_ condition of induction (\(I\rightarrow\
eg q\)) holds by construction, whereas the algorithm must check whether or not the _relative consecution_ condition (\(F_{j-1}\wedge\
eg q\wedge T\rightarrow\
eg q^{\prime}\)) holds. This can be performed by proving that the following SAT query is unsatisfiable (line 7):  
\[SAT(F_{j-1}\wedge\
eg q\wedge T\wedge q^{\prime}) \tag{59}\]  
If relative consecution holds (i.e., Query (59) is UNSAT), then the clause \(\
eg q\) is inductive relative to \(F_{j-1}\) and can be used to refine \(F_{j}\), ruling out \(q\) (lines 10-13). To pursue a stronger refinement of \(F_{j}\), the inductive clause found undergoes a process called _inductive generalization_ (line 11) prior to being added to the frame. Inductive generalization is carried out by the \(\textsc{Generalize}(j,q,\mathbf{F_{k}})\) procedure, described in Algorithm 8, which tries to minimize the number of literals in a clause \(c=\
eg q\) while maintaining its inductiveness relative to \(F_{j-1}\), in order to preserve monotonicity. The resulting clause is added not only to \(F_{j}\), but also to every frame \(F_{i},\ 0<i<j\) (line 12). Doing so discharges the proof obligation \((q,j)\) ruling out \(q\) from every \(F_{i}\) with \(0<i\leq j\). Since the sets \(F_{i}\) with \(i>j\) are larger than \(F_{j}\), \(q\) may still be present in one of them and \((q,j+1)\) may become a new proof obligation. To address this issue, Algorithm 7 adds \((q,j+1)\) to the proof-obligations queue (line 13). Figure 8e,f visualize this step. Otherwise, if the relative consecution does not hold (see Figure 8c), there is a predecessor \(s\) of \(q\) in \(F_{j-1}\wedge\
eg q\). Such predecessors are called _counterexamples to the inductiveness_ (CTIs). To preserve image approximation, before blocking a cube \(q\) in a frame \(F_{j}\), every CTI of \(q\) must be blocked in \(F_{j-1}\) (Figure 8d). Therefore, the CTI \(s\) is first extended into a cube \(p\) (line 8), and then both proof obligations \((p,j-1)\) and \((q,j)\) are added to the queue (line 9). The \(\textsc{Generalize}(j,q,\mathbf{F_{k}})\) procedure (Algorithm 8) performs inductive generalization, which is a fundamental step of the algorithm. During inductive generalization, given a clause \(\
eg q\) relative inductive to \(F_{j-1}\), IC3 tries to compute a clause \(c\) subset of \(\
eg q\) such that \(c\) is still inductive relative to \(F_{j-1}\). Acting this way, and using \(c\) to refine the frames, the algorithm can block not only the original bad cube \(q\) but potentially also other states, which in turn may lead to faster convergence. Inductive generalization works by dropping literals from the input clause while maintaining relative inductiveness with respect to \(F_{j-1}\).