diff --git a/test/formal/byte_big.py b/test/formal/byte_big.py
index db11bc998..8e6dfd7ef 100644
--- a/test/formal/byte_big.py
+++ b/test/formal/byte_big.py
@@ -1,5 +1,6 @@
+from opcodes import BYTE
 from rule import Rule
-from opcodes import *
+from z3 import BitVec
 
 """
 byte(A, X) -> 0
diff --git a/test/formal/byte_equivalence.py b/test/formal/byte_equivalence.py
index 0f3638424..c607eca4c 100644
--- a/test/formal/byte_equivalence.py
+++ b/test/formal/byte_equivalence.py
@@ -1,5 +1,6 @@
+from opcodes import BYTE
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal, Concat, Extract
 
 """
 Checks that the byte opcode (implemented using shift) is equivalent to a
diff --git a/test/formal/checked_int_add.py b/test/formal/checked_int_add.py
index 6e74944e2..43368a98d 100644
--- a/test/formal/checked_int_add.py
+++ b/test/formal/checked_int_add.py
@@ -1,6 +1,7 @@
+from opcodes import AND, ISZERO, SGT, SLT, SUB
 from rule import Rule
-from opcodes import *
-from util import *
+from util import BVSignedMax, BVSignedMin, BVSignedUpCast
+from z3 import BitVec, BVAddNoOverflow, BVAddNoUnderflow, Not
 
 """
 Overflow checked signed integer addition.
diff --git a/test/formal/checked_int_div.py b/test/formal/checked_int_div.py
index 2a36a9488..4c9d4e829 100644
--- a/test/formal/checked_int_div.py
+++ b/test/formal/checked_int_div.py
@@ -1,6 +1,7 @@
+from opcodes import AND, EQ, SUB
 from rule import Rule
-from opcodes import *
-from util import *
+from util import BVSignedMin, BVSignedUpCast
+from z3 import BitVec, BVSDivNoOverflow, Not
 
 """
 Overflow checked signed integer division.
diff --git a/test/formal/checked_int_mul_16.py b/test/formal/checked_int_mul_16.py
index cc8743b1d..b2f9eb852 100644
--- a/test/formal/checked_int_mul_16.py
+++ b/test/formal/checked_int_mul_16.py
@@ -1,6 +1,7 @@
+from opcodes import AND, DIV, GT, SDIV, SGT, SLT
 from rule import Rule
-from opcodes import *
-from util import *
+from util import BVSignedMax, BVSignedMin, BVSignedUpCast
+from z3 import BVMulNoOverflow, BVMulNoUnderflow, BitVec, Not, Or
 
 """
 Overflow checked signed integer multiplication.
diff --git a/test/formal/checked_int_sub.py b/test/formal/checked_int_sub.py
index 72a0a2109..ed292bbe0 100644
--- a/test/formal/checked_int_sub.py
+++ b/test/formal/checked_int_sub.py
@@ -1,6 +1,7 @@
+from opcodes import AND, ADD, ISZERO, SLT, SGT
 from rule import Rule
-from opcodes import *
-from util import *
+from util import BVSignedMax, BVSignedMin, BVSignedUpCast
+from z3 import BitVec, BVSubNoOverflow, BVSubNoUnderflow, Not
 
 """
 Overflow checked signed integer subtraction.
diff --git a/test/formal/checked_uint_add.py b/test/formal/checked_uint_add.py
index 596fa04f0..e38b4dcdb 100644
--- a/test/formal/checked_uint_add.py
+++ b/test/formal/checked_uint_add.py
@@ -1,6 +1,7 @@
+from opcodes import GT, SUB
 from rule import Rule
-from opcodes import *
-from util import *
+from util import BVUnsignedMax, BVUnsignedUpCast
+from z3 import BitVec, BVAddNoOverflow, Not
 
 """
 Overflow checked unsigned integer addition.
diff --git a/test/formal/checked_uint_mul_16.py b/test/formal/checked_uint_mul_16.py
index 6e8901799..1c60de47b 100644
--- a/test/formal/checked_uint_mul_16.py
+++ b/test/formal/checked_uint_mul_16.py
@@ -1,6 +1,7 @@
+from opcodes import AND, ISZERO, GT, DIV
 from rule import Rule
-from opcodes import *
-from util import *
+from util import BVUnsignedUpCast, BVUnsignedMax
+from z3 import BitVec, Not, BVMulNoOverflow
 
 """
 Overflow checked unsigned integer multiplication.
diff --git a/test/formal/checked_uint_sub.py b/test/formal/checked_uint_sub.py
index b0f25b582..65bcf74a4 100644
--- a/test/formal/checked_uint_sub.py
+++ b/test/formal/checked_uint_sub.py
@@ -1,6 +1,7 @@
+from opcodes import LT
 from rule import Rule
-from opcodes import *
-from util import *
+from util import BVUnsignedMax, BVUnsignedUpCast
+from z3 import BVSubNoUnderflow, BitVec, Not
 
 """
 Overflow checked unsigned integer subtraction.
diff --git a/test/formal/combine_byte_shl.py b/test/formal/combine_byte_shl.py
index e2a6034ff..f492cc18f 100644
--- a/test/formal/combine_byte_shl.py
+++ b/test/formal/combine_byte_shl.py
@@ -1,5 +1,6 @@
+from opcodes import BYTE, SHL
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, ULE
 
 """
 byte(A, shl(B, X))
diff --git a/test/formal/combine_byte_shr_1.py b/test/formal/combine_byte_shr_1.py
index 4938e73f7..788319aa2 100644
--- a/test/formal/combine_byte_shr_1.py
+++ b/test/formal/combine_byte_shr_1.py
@@ -1,5 +1,6 @@
+from opcodes import BYTE, DIV, SHR
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, UGE, ULE, ULT
 
 """
 byte(A, shr(B, X))
diff --git a/test/formal/combine_byte_shr_2.py b/test/formal/combine_byte_shr_2.py
index 4f9be05a4..d969c301b 100644
--- a/test/formal/combine_byte_shr_2.py
+++ b/test/formal/combine_byte_shr_2.py
@@ -1,5 +1,6 @@
+from opcodes import BYTE, SHR, DIV
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, ULT
 
 """
 byte(A, shr(B, X))
diff --git a/test/formal/combine_div_shl_one_32.py b/test/formal/combine_div_shl_one_32.py
index 2ee7d2137..5cca7288b 100644
--- a/test/formal/combine_div_shl_one_32.py
+++ b/test/formal/combine_div_shl_one_32.py
@@ -1,5 +1,6 @@
+from opcodes import DIV, SHL, SHR
 from rule import Rule
-from opcodes import *
+from z3 import BitVec
 
 """
 Rule:
diff --git a/test/formal/combine_mul_shl_one_64.py b/test/formal/combine_mul_shl_one_64.py
index 44d031b98..169cc5be0 100644
--- a/test/formal/combine_mul_shl_one_64.py
+++ b/test/formal/combine_mul_shl_one_64.py
@@ -1,5 +1,6 @@
+from opcodes import SHL, MUL
 from rule import Rule
-from opcodes import *
+from z3 import BitVec
 
 """
 Rule:
diff --git a/test/formal/combine_shl_shr_by_constant_64.py b/test/formal/combine_shl_shr_by_constant_64.py
index fc7ec64e8..4d8e6a1f8 100644
--- a/test/formal/combine_shl_shr_by_constant_64.py
+++ b/test/formal/combine_shl_shr_by_constant_64.py
@@ -1,5 +1,6 @@
+from opcodes import AND, SHL, SHR
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal, If, Int2BV, IntVal, UGT, ULT
 
 """
 Rule:
diff --git a/test/formal/combine_shr_shl_by_constant_64.py b/test/formal/combine_shr_shl_by_constant_64.py
index c011a2616..5bc852574 100644
--- a/test/formal/combine_shr_shl_by_constant_64.py
+++ b/test/formal/combine_shr_shl_by_constant_64.py
@@ -1,5 +1,6 @@
+from opcodes import AND, SHL, SHR
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal, If, Int2BV, IntVal, UGT, ULT
 
 """
 Rule:
diff --git a/test/formal/eq_sub.py b/test/formal/eq_sub.py
index bf7518acf..76808bc3b 100644
--- a/test/formal/eq_sub.py
+++ b/test/formal/eq_sub.py
@@ -1,5 +1,6 @@
+from opcodes import EQ, ISZERO, SUB
 from rule import Rule
-from opcodes import *
+from z3 import BitVec
 
 """
 Rule:
diff --git a/test/formal/exp_neg_one.py b/test/formal/exp_neg_one.py
index 88416496e..4dffb88b0 100644
--- a/test/formal/exp_neg_one.py
+++ b/test/formal/exp_neg_one.py
@@ -1,6 +1,7 @@
+from opcodes import AND, ISZERO, MOD, SUB
 from rule import Rule
-from opcodes import *
-from util import *
+from util import BVUnsignedMax
+from z3 import BitVec, BitVecVal, If
 
 """
 Checking conversion of exp(-1, X) to sub(isZero(and(X, 1)), and(X, 1))
diff --git a/test/formal/exp_to_shl.py b/test/formal/exp_to_shl.py
index 064d1af3e..499cf7c2f 100644
--- a/test/formal/exp_to_shl.py
+++ b/test/formal/exp_to_shl.py
@@ -1,6 +1,6 @@
+from opcodes import SHL
 from rule import Rule
-from opcodes import *
-from util import *
+from z3 import BitVec, If
 
 """
 Checking conversion of exp(2, X) to shl(X, 1)
diff --git a/test/formal/move_and_across_shl_128.py b/test/formal/move_and_across_shl_128.py
index d3f5c3a66..9e689b71e 100644
--- a/test/formal/move_and_across_shl_128.py
+++ b/test/formal/move_and_across_shl_128.py
@@ -1,5 +1,6 @@
+from opcodes import AND, SHL
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal, ULT
 
 """
 Rule:
diff --git a/test/formal/move_and_across_shr_128.py b/test/formal/move_and_across_shr_128.py
index 7ec4a65c1..592dc7742 100644
--- a/test/formal/move_and_across_shr_128.py
+++ b/test/formal/move_and_across_shr_128.py
@@ -1,5 +1,6 @@
+from opcodes import AND, SHR
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal, ULT
 
 """
 Rule:
diff --git a/test/formal/move_and_inside_or.py b/test/formal/move_and_inside_or.py
index 09dc35c51..48ec20dba 100644
--- a/test/formal/move_and_inside_or.py
+++ b/test/formal/move_and_inside_or.py
@@ -1,5 +1,7 @@
+from opcodes import AND, OR
 from rule import Rule
-from opcodes import *
+from z3 import BitVec
+
 
 """
 Rule:
diff --git a/test/formal/opcodes.py b/test/formal/opcodes.py
index 6098d01ed..103e57a14 100644
--- a/test/formal/opcodes.py
+++ b/test/formal/opcodes.py
@@ -1,4 +1,4 @@
-from z3 import *
+from z3 import BitVecVal, BV2Int, If, LShR, UDiv, ULT, UGT, URem
 
 def ADD(x, y):
 	return x + y
diff --git a/test/formal/repeated_and.py b/test/formal/repeated_and.py
index 2e8431b3c..2376ca34f 100644
--- a/test/formal/repeated_and.py
+++ b/test/formal/repeated_and.py
@@ -1,5 +1,6 @@
+from opcodes import AND
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal
 
 """
 Rule:
diff --git a/test/formal/repeated_or.py b/test/formal/repeated_or.py
index c1b2ebd09..ba18e39aa 100644
--- a/test/formal/repeated_or.py
+++ b/test/formal/repeated_or.py
@@ -1,5 +1,6 @@
+from opcodes import OR
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal
 
 """
 Rule:
diff --git a/test/formal/replace_mul_by_shift.py b/test/formal/replace_mul_by_shift.py
index 5a2c2dc14..3805af0dc 100644
--- a/test/formal/replace_mul_by_shift.py
+++ b/test/formal/replace_mul_by_shift.py
@@ -1,5 +1,6 @@
+from opcodes import DIV, MUL, SHL, SHR
 from rule import Rule
-from opcodes import *
+from z3 import BitVec
 
 """
 Rule:
diff --git a/test/formal/rule.py b/test/formal/rule.py
index 9327f7e5a..ac0f0c8a6 100644
--- a/test/formal/rule.py
+++ b/test/formal/rule.py
@@ -1,6 +1,6 @@
 import sys
 
-from z3 import *
+from z3 import sat, Solver, unknown, unsat
 
 class Rule:
 	def __init__(self):
diff --git a/test/formal/shl_workaround_8.py b/test/formal/shl_workaround_8.py
index 2ca711cdf..19248574a 100644
--- a/test/formal/shl_workaround_8.py
+++ b/test/formal/shl_workaround_8.py
@@ -1,5 +1,6 @@
+from opcodes import SHL
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BV2Int, Int2BV, IntVal
 
 """
 Shift left workaround that Solidity implements
diff --git a/test/formal/signextend.py b/test/formal/signextend.py
index 483fcca56..ed285345d 100644
--- a/test/formal/signextend.py
+++ b/test/formal/signextend.py
@@ -1,5 +1,6 @@
+from opcodes import SIGNEXTEND
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal, If, UGE, ULT
 
 """
 Rule:
diff --git a/test/formal/signextend_and.py b/test/formal/signextend_and.py
index ae2b4bd2c..91fc14349 100644
--- a/test/formal/signextend_and.py
+++ b/test/formal/signextend_and.py
@@ -1,5 +1,6 @@
+from opcodes import SIGNEXTEND, AND
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal, ULT
 
 """
 Rule:
diff --git a/test/formal/signextend_equivalence.py b/test/formal/signextend_equivalence.py
index 1199fff47..3b8386e54 100644
--- a/test/formal/signextend_equivalence.py
+++ b/test/formal/signextend_equivalence.py
@@ -1,5 +1,6 @@
+from opcodes import SIGNEXTEND
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal, Extract, SignExt, UGT
 
 """
 Checking the implementation of SIGNEXTEND using Z3's native SignExt and Extract
diff --git a/test/formal/signextend_shl.py b/test/formal/signextend_shl.py
index 608b10eec..18b1baea1 100644
--- a/test/formal/signextend_shl.py
+++ b/test/formal/signextend_shl.py
@@ -1,5 +1,6 @@
+from opcodes import SHL, SIGNEXTEND
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, LShR, ULE
 
 """
 Rule:
diff --git a/test/formal/signextend_shr.py b/test/formal/signextend_shr.py
index aa44a2345..a763314cd 100644
--- a/test/formal/signextend_shr.py
+++ b/test/formal/signextend_shr.py
@@ -1,5 +1,6 @@
+from opcodes import SIGNEXTEND, SAR, SHR
 from rule import Rule
-from opcodes import *
+from z3 import BitVec,  BitVecVal, ULE
 
 """
 Rule:
diff --git a/test/formal/sub_not_zero_x_to_not_x_256.py b/test/formal/sub_not_zero_x_to_not_x_256.py
index eb3301100..d8f1282ec 100644
--- a/test/formal/sub_not_zero_x_to_not_x_256.py
+++ b/test/formal/sub_not_zero_x_to_not_x_256.py
@@ -1,5 +1,6 @@
+from opcodes import NOT, SUB
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal
 
 """
 Rule:
diff --git a/test/formal/sub_sub.py b/test/formal/sub_sub.py
index d6099c91f..643941085 100644
--- a/test/formal/sub_sub.py
+++ b/test/formal/sub_sub.py
@@ -1,5 +1,6 @@
+from opcodes import ADD, SUB
 from rule import Rule
-from opcodes import *
+from z3 import BitVec
 
 """
 Rules:
diff --git a/test/formal/util.py b/test/formal/util.py
index 8331a1fcc..8d0debbef 100644
--- a/test/formal/util.py
+++ b/test/formal/util.py
@@ -1,4 +1,4 @@
-from z3 import *
+from z3 import BitVecVal, Concat, If
 
 def BVUnsignedUpCast(x, n_bits):
 	assert x.size() <= n_bits