// Date: 19.05.2013
// Author: heizmann@informatik.uni-freiburg.de


parseAutomata("../nwa/ProgramVerification-Ministerprasident.ats");

assert(numberOfStates(differenceSenwa(McCarthyInterpolantAutomaton_Iteration16, McCarthyInterpolantAutomaton_Iteration12)) == 126);
assert(numberOfStates(differenceSenwa(McCarthyAbstraction16, McCarthyInterpolantAutomaton_Iteration12)) == 377);
assert(numberOfStates(differenceSenwa(McCarthyAbstraction16, McCarthyInterpolantAutomaton_Iteration16)) == 377);

assert(numberOfStates(differenceSenwa(Ackermann_Abstraction24, Ackermann_InterpolantAutomaton_Iteration39)) == 544);
assert(numberOfStates(differenceSenwa(Ackermann_Abstraction19, Ackermann_InterpolantAutomaton_Iteration39)) == 123);