Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

uext crashes with -1 (overflow?) #5

Closed
deian opened this issue Oct 16, 2018 · 1 comment
Closed

uext crashes with -1 (overflow?) #5

deian opened this issue Oct 16, 2018 · 1 comment

Comments

@deian
Copy link
Member

deian commented Oct 16, 2018

@mlfbrown discovered this

import qualified Boolector as Bimport Control.Monad.IO.Class
import Control.Exception (assert)
import Control.Concurrent

main :: IO ()
main = do
 -- Create new Boolector state with a 1s timeout
 bs <- B.newBoolectorState (Just 1)
 B.evalBoolector bs $ do
   -- Create a 8-bit bit-vector
   u8 <- B.bitvecSort 8   -- Create a constant value and two variables of sort u8
   c <- B.unsignedInt 35 u8
   B.uext c 4294967289 -- Crashes in this case but is fine with, say, 87; 88 crashes with > 0 bounds check
   return ()
@deian
Copy link
Member Author

deian commented Oct 16, 2018

Fixed in boolector: Boolector/boolector@c6de121

@deian deian closed this as completed Oct 16, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant