Fix address space limit test. Fixes #243

smowton · smowton · commit 49c4b3ac06d6 · 2017-01-25T11:41:33.000Z
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
@@ -795,7 +795,7 @@ void bv_pointerst::add_addr(const exprt &expr, bvt &bv)
 {
   std::size_t a=pointer_logic.add_object(expr);
 
-  if(a==(std::size_t(1)>>object_bits))
+  if(a==(std::size_t(1)<<object_bits))
     throw "too many variables";
 
   encode(a, bv);

Original file line number	Diff line number	Diff line change
`@@ -795,7 +795,7 @@ void bv_pointerst::add_addr(const exprt &expr, bvt &bv)`
`795`	`795`	`{`
`796`	`796`	`std::size_t a=pointer_logic.add_object(expr);`
`797`	`797`
`798`		`- if(a==(std::size_t(1)>>object_bits))`
	`798`	`+ if(a==(std::size_t(1)<<object_bits))`
`799`	`799`	`throw "too many variables";`
`800`	`800`
`801`	`801`	`encode(a, bv);`