Does the dReal SMT solver return counterexamples? I have seen examples where :produce-models is true, but I do not know how to generate counterexamples. Also, the dReach tool has a --visualize option, so it would seem that dReal would need to produce some model information. However, when I run it on .smt2 files, I can't seem to find a way to view counterexamples.
Asked
Active
Viewed 126 times
1 Answers
1
O.k., it is trivial :). dReal does not follow the usual .smt2 convention of using (get-model), but you can get models by using the command line option --model.
E.g.: dReal --model microwave1.smt2
Mike Whalen
- 33
- 4