CODEWITHSUNDEEP
pythonz3smtz3py
0xTomato
0xTomato

Reputation: 116

BitVecVal not found as an attribute to z3

I am trying to use Python API of z3, one of the more popular SMT solvers, to create an SMT instance. To begin, I would like to create four bit vectors with two bits and values ranging from zero to three. My initialization code in Python is the following:

import z3

NONE = z3.BitVecVal(0, 2)
A    = z3.BitVecVal(1, 2)
B    = z3.BitVecVal(2, 2)
C    = z3.BitVecVal(3, 2)

But I encountered this error when running the Python file: AttributeError: module 'z3' has no attribute 'BitVecVal'. I looked up BitVecVal and it is a valid instance of z3, shown here. Any ideas how to fix this?

Upvotes: 1

Views: 1145

Answers (3)

wei wei
wei wei

Reputation: 11

I have the same problem in Pycharm IDE (when I only install z3 from file->setting-> Project Interpreter -> add ) But after the I install z3-solver, this problem is resolved.

Upvotes: 1

alias
alias

Reputation: 30428

There's nothing wrong with your program. I added a print version at the beginning and a print statement at the end:

import z3

print z3.get_version_string()

NONE = z3.BitVecVal(0, 2)
A    = z3.BitVecVal(1, 2)
B    = z3.BitVecVal(2, 2)
C    = z3.BitVecVal(3, 2)

print  NONE, A, B, C

And I get:

4.8.8
0 1 2 3

This suggests your installation is somehow busted. Your best bet might be to reinstall from scratch.

Upvotes: 1

0xTomato
0xTomato

Reputation: 116

The z3 package is likely not imported correctly. Make sure you are in the right environment when executing the Python code.

Upvotes: 0

Related Questions