Fix the simplest pylint warnings (variables/imports, semicolons, etc) and re-enable them in pylintrc

test/formal/move_and_across_shr_128.py

@@ -25,12 +25,12 @@ BitWidth = BitVecVal(n_bits, n_bits)
 rule.require(ULT(B, BitWidth))
 
 # Non optimized result
-nonopt_1 = SHR(B, AND(X, A));
-nonopt_2 = SHR(B, AND(A, X));
+nonopt_1 = SHR(B, AND(X, A))
+nonopt_2 = SHR(B, AND(A, X))
 
 # Optimized result
-Mask = SHR(B, A);
-opt = AND(SHR(B, X), Mask);
+Mask = SHR(B, A)
+opt = AND(SHR(B, X), Mask)
 
 rule.check(nonopt_1, opt)
 rule.check(nonopt_2, opt)

test/formal/signextend.py

@@ -34,4 +34,3 @@ rule3.check(
     SIGNEXTEND(A, SIGNEXTEND(B, X)),
     SIGNEXTEND(If(ULT(A, B), A, B), X)
 )
-

test/formal/signextend_shr.py

@@ -28,4 +28,3 @@ rule.check(
     SIGNEXTEND(A, SHR(B, X)),
     SAR(B, X)
 )
-

test/formal/util.py

@@ -1,27 +1,27 @@
 from z3 import *
 
 def BVUnsignedUpCast(x, n_bits):
-	assert(x.size() <= n_bits)
+	assert x.size() <= n_bits
 	if x.size() < n_bits:
 		return Concat(BitVecVal(0, n_bits - x.size()), x)
 	else:
 		return x
 
 def BVUnsignedMax(type_bits, n_bits):
-	assert(type_bits <= n_bits)
+	assert type_bits <= n_bits
 	return BitVecVal((1 << type_bits) - 1, n_bits)
 
 def BVSignedUpCast(x, n_bits):
-	assert(x.size() <= n_bits)
+	assert x.size() <= n_bits
 	if x.size() < n_bits:
 		return Concat(If(x < 0, BitVecVal(-1, n_bits - x.size()), BitVecVal(0, n_bits - x.size())), x)
 	else:
 		return x
 
 def BVSignedMax(type_bits, n_bits):
-	assert(type_bits <= n_bits)
+	assert type_bits <= n_bits
 	return BitVecVal((1 << (type_bits - 1)) - 1, n_bits)
 
 def BVSignedMin(type_bits, n_bits):
-	assert(type_bits <= n_bits)
+	assert type_bits <= n_bits
 	return BitVecVal(-(1 << (type_bits - 1)), n_bits)