This commit is contained in:
Rob Dockins 2020-05-18 10:44:54 -07:00 committed by robdockins
parent 60dcbd1d40
commit 1b584d9567
2 changed files with 2 additions and 2 deletions

View File

@ -303,7 +303,7 @@ instance Backend SBV where
do unless (0 <= e) (raiseError sym NegativeExponent)
pure $! SBV.svExp a b
| otherwise =
liftIO (X.throw (UnsupportedSymbolicOp "integer exponentation"))
liftIO (X.throw (UnsupportedSymbolicOp "integer exponentiation"))
-- NB, we don't do reduction here
intToZn _ _m a = pure a

View File

@ -299,7 +299,7 @@ instance W4.IsExprBuilder sym => Backend (What4 sym) where
intExp (What4 sym) x y
| Just i <- W4.asInteger y = intExpConcrete sym x i
| otherwise = liftIO (X.throw (UnsupportedSymbolicOp "integer exponentation"))
| otherwise = liftIO (X.throw (UnsupportedSymbolicOp "integer exponentiation"))
intLg2 (What4 sym) x
| Just i <- W4.asInteger x = liftIO $ W4.intLit sym (lg2 i)