Parsing of MPSat output for reachability analysis has an error

[Danil Sokolov]

Load the attached a.work file and try checking reachability for the following two Reach expressions:

let full=PP"notreal" {
  card full=0
}

let full=PP"notreal" {
  card full>0
}

Both expressions give the same result - "the property is satisfied". This is incorrect as the expressions are mutually exclusive.

The reason for error is incorrect parsing of MPSat output, in particular the ignoring this form of solution report:

...
 Trivial case

SOLUTION 0:
total cost of all paths: 0

the predicate is satisfiable
...