When you haven't written enough constraints, and are allow absurd - solutions which shouldn't even be considered, then you are facing - a problem of underconsrtaint. This kind of bug is actually pretty +
When you haven't written enough constraints, you allow absurd + solutions which shouldn't have been allowed. This is the + problem of underconsrtaint. This kind of bug is actually pretty easy to catch. You'll spot it when you get a bogus counterexample; one that shouldn't exist at all, and thus isn't a - legitimate counterexample. Look at it and formulate why it + legitimate example. Look at it and formulate why it is ill-formed, then simply add a constraint to prevent solutions of that form. However, make sure that the situation can't actually occur in the system you are modeling, and be wary of ruling out desirable solutions in your effort to prevent the bad - one that you have found.
- -You can use the run command help identify - underconstraints.
+ one that you have found.(ie. avoid overconstraining) +You can use the run command to help identify + underconstraints from examples .
+You can also use the check command on assertions to check that no wrong examples (counterexamples) exist.
The other side of the coin is overconstraint.