From d0ca2fd3211f3bc0cfc582df978b6a82ea7ec390 Mon Sep 17 00:00:00 2001
From: Hristina Palikareva <h.palikareva@imperial.ac.uk>
Date: Wed, 3 Dec 2014 13:43:44 +0000
Subject: Handling overshift behaviour in MetaSMTBuilder

---
 lib/Solver/MetaSMTBuilder.h | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
index b5c99907..458c55ba 100644
--- a/lib/Solver/MetaSMTBuilder.h
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -499,6 +499,11 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarLeftShif
                                                     bvLeftShift(expr, width, i, shiftBits),
                                                     res));
     }
+    
+    // If overshifting, shift to zero    
+    res = evaluate(_solver, metaSMT::logic::Ite(bvult(shift, bvConst32(shiftBits, width)),
+                                                res,
+                                                bvZero(width)));                                                
 
     return(res);
 }
@@ -521,6 +526,11 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarRightShi
                                                     res));
          // ToDo Reconsider widht to provide to bvRightShift
     }
+    
+    // If overshifting, shift to zero
+    res = evaluate(_solver, metaSMT::logic::Ite(bvult(shift, bvConst32(shiftBits, width)),
+                                                res,
+                                                bvZero(width)));                                                
 
     return(res);
 }
@@ -548,6 +558,11 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarArithRig
                                                     constructAShrByConstant(expr, width, i, signedBool, shiftBits),
                                                     res));
     }
+    
+    // If overshifting, shift to zero
+    res = evaluate(_solver, metaSMT::logic::Ite(bvult(shift, bvConst32(shiftBits, width)),
+                                                res,
+                                                bvZero(width)));      
 
     return(res);
 }
-- 
cgit 1.4.1