Check if model satisfies constraints

[egolf-cs]

What is the proper way to check if a model, m, satisfies the constraints of a Solver object?

One way to do this check:

1. Construct constraint c that is satisfied only by m
2. push
3. add constraint c
4. check if sat
5. pop
6. m satisfies the constraints iff the check in 4 was sat

Is this the best way to do this?

[NikolajBjorner]

• you can sometimes use the eval function on models to simplify constraints using a model