diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-09-16 08:54:03 +0100 |
---|---|---|
committer | Dan Liew <delcypher@gmail.com> | 2017-06-01 11:36:09 +0100 |
commit | 1311a933232642299fa3593d9f7766e26ae66d3b (patch) | |
tree | 05d7b6e0952fcdfc681162dfe4f7562cfda7f282 /TODO.txt | |
parent | 66e3b6b3dcbf38f5cb4bed7aba57e89ff296c468 (diff) | |
download | klee-1311a933232642299fa3593d9f7766e26ae66d3b.tar.gz |
[Z3] Add option to manually validate Z3 models.
This can be enabled by passing the command line option `-debug-z3-validate-models`. Although Z3 has a global parameter `model_validate` (off by default) I don't trust it so do the validation manually. This also means we can potentially do validation on a per Z3Solver instance basis rather than globally. When failing to validate a Z3 model the solver state and model are dumped to standard error.
Diffstat (limited to 'TODO.txt')
0 files changed, 0 insertions, 0 deletions