about summary refs log tree commit diff homepage
path: root/TODO.txt
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2016-09-16 08:54:03 +0100
committerDan Liew <delcypher@gmail.com>2017-06-01 11:36:09 +0100
commit1311a933232642299fa3593d9f7766e26ae66d3b (patch)
tree05d7b6e0952fcdfc681162dfe4f7562cfda7f282 /TODO.txt
parent66e3b6b3dcbf38f5cb4bed7aba57e89ff296c468 (diff)
downloadklee-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