Infinite loop detector: Improve SMT solver template

[JoeyChenSmart]

The current template being used by the SMT solver can possibly be improved: instead of "Path -> Transition -> Path", perhaps "(Path & Transition) -> Path" is better. (More elaboration below)

e.g. in

function f(x) {
  if (x === 0) { return 0; }
  if (x < 0) { return f(- (x - 1)); }
  else { return f(- (x + 1)); }
}

f(1);

Currently the SMT code is:

forall x,x':int.
(x > 0 and x >=0) or (x < 0 and x < 0)
-> (x' = -(x + 1)) or (x' = -(x-1))
-> (x' > 0 and x' >=0) or (x' < 0 and x' < 0)

which does not catch the above example, and perhaps changing it to:

forall x,x':int.
(x > 0 and x >=0 and x' = -(x + 1)) or (x < 0 and x < 0 and x' = -(x-1))
-> (x' > 0 and x' >=0) or (x' < 0 and x' < 0)

will help.

This is a minor issue since most programs will not have these 'alternating paths' (i.e. the SMT code will not have 'or's).

Will also have to look into whether the proposed new template introduces any errors/false positives.