overflow in naturals leads to unsatisfiable constraint

[abau]

An overflow in a natural number inside a branch of a case-distinction leads to an unsatisfiable constraint no matter if the branch is chosen or not. Instead, an overflow should result in a undefined value (definedness flag being set to False).

Test case

constraint c = case c of
  True  -> False && (geNat (nat 1 1) (plusNat (nat 1 1) (nat 1 1)))
  False -> True

should give a solution c = False despite of the overflow in the True branch.