Cardinality aggregate with simplified formula can lead to errors

E.g., the following specification returns an error from Idp_to_Z3.

vocabulary V {
    type Foo := {1, 2, 3}
    bar: Foo -> Foo
    bop: Foo -> Bool
}

theory {
    #{f in Foo: bar(f) = 1 & bop(f)} = 2.
}

structure {
    bop := {1, 2}. 
}

procedure main() {
    pretty_print(model_expand(T,S))
}

Essentially, the new optimized method for translating formulas of the form #{t in Type: phi(t)} = num has a bug when phi(t) has been simplified during grounding, as in the example above.