Merge pull request #158 from jad-hamza/bitset-fix2

samarion · web-flow · commit 2f66f5ab53f2 · 2021-06-28T16:13:15.000+02:00
When shifting right, only add ones for signed bitvectors
diff --git a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
@@ -302,7 +302,7 @@ trait RecursiveEvaluator
         case (BVLiteral(sig1, i1, s1), b2 @ BVLiteral(sig2, _, s2)) if sig1 == sig2 && s1 == s2 =>
           val shiftCount = b2.toBigInt.toInt
           val shifted = shift(i1, s1, -shiftCount)
-          BVLiteral(sig1, if (i1(s1)) shifted ++ ((s1 - shiftCount) to s1) else shifted, s1)
+          BVLiteral(sig1, if (i1(s1) && sig1) shifted ++ ((s1 - shiftCount) to s1) else shifted, s1)
         case (le,re) => throw EvalError("Unexpected operation: (" + le.asString + ") >> (" + re.asString + ")")
       }
 

Original file line number	Diff line number	Diff line change
`@@ -302,7 +302,7 @@ trait RecursiveEvaluator`
`302`	`302`	`case (BVLiteral(sig1, i1, s1), b2 @ BVLiteral(sig2, _, s2)) if sig1 == sig2 && s1 == s2 =>`
`303`	`303`	`val shiftCount = b2.toBigInt.toInt`
`304`	`304`	`val shifted = shift(i1, s1, -shiftCount)`
`305`		`- BVLiteral(sig1, if (i1(s1)) shifted ++ ((s1 - shiftCount) to s1) else shifted, s1)`
	`305`	`+ BVLiteral(sig1, if (i1(s1) && sig1) shifted ++ ((s1 - shiftCount) to s1) else shifted, s1)`
`306`	`306`	`case (le,re) => throw EvalError("Unexpected operation: (" + le.asString + ") >> (" + re.asString + ")")`
`307`	`307`	`}`
`308`	`308`