ilang::LegacyBmc Class Reference

Simplified bounded model checking engine for ILAs. More...

#include <v_eq_check_legacy_bmc.h>

Public Member Functions
	LegacyBmc ()
	Default constructor.
	~LegacyBmc ()
	Default destructor.
void	AddInit (ExprPtr init)
	Add initial condition to the solver.
void	AddInvariant (ExprPtr inv)
	Add invariant to the solver.
void	AddProperty (ExprPtr prop)
	Add property of one ILA.
z3::check_result	Check (InstrLvlAbsPtr m0, const int &k0, InstrLvlAbsPtr m1, const int &k1)
	Legacy BMC where two ILAs are unrolled and compared monolithically.

Detailed Description

Simplified bounded model checking engine for ILAs.

---

The documentation for this class was generated from the following file:

• v_eq_check_legacy_bmc.h