diff options
| author | Hristina Palikareva <h.palikareva@imperial.ac.uk> | 2013-10-08 16:55:10 +0100 |
|---|---|---|
| committer | Hristina Palikareva <h.palikareva@imperial.ac.uk> | 2013-10-11 20:02:33 +0100 |
| commit | d508fcc715277ea0a22c007ecde6ebc991d81841 (patch) | |
| tree | ed5c0c6a8b9faff56428051ae10928adb66b66ad /lib/Solver/MetaSMTBuilder.h | |
| parent | 64868646eed7384c38db41aff5002215b92c1601 (diff) | |
| download | klee-d508fcc715277ea0a22c007ecde6ebc991d81841.tar.gz | |
Bug fix in MetaSMTBuilder
Diffstat (limited to 'lib/Solver/MetaSMTBuilder.h')
| -rw-r--r-- | lib/Solver/MetaSMTBuilder.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index 0e508b46..2b084ac7 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -928,8 +928,8 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu if (*width_out == 1) { res = evaluate(_solver, metaSMT::logic::Not(child)); } - else { - res = evaluate(_solver, bvneg(child)); + else { + res = evaluate(_solver, bvnot(child)); } break; } |