about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
authorHristina Palikareva <h.palikareva@imperial.ac.uk>2013-10-08 16:55:10 +0100
committerHristina Palikareva <h.palikareva@imperial.ac.uk>2013-10-11 20:02:33 +0100
commitd508fcc715277ea0a22c007ecde6ebc991d81841 (patch)
treeed5c0c6a8b9faff56428051ae10928adb66b66ad /lib/Solver
parent64868646eed7384c38db41aff5002215b92c1601 (diff)
downloadklee-d508fcc715277ea0a22c007ecde6ebc991d81841.tar.gz
Bug fix in MetaSMTBuilder
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/MetaSMTBuilder.h4
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;	  
         }