When I run DNNF-GHPR benchmark, I receive the following error (the complete error is list is in the attachment:

dnnf properties/dronet_property_0.py --network N onnx/dronet.onnx --backend cleverhans.projected_gradient_descent
Falsifying: Forall(x, (((0 <= x) & (x <= 1) & (N(slice(2, -3, None), 1) <= -2.1972245773362196)) ==> ((-0.08726646259971647 <= N(slice(2, -1, None), 0)) & (N(slice(2, -1, None), 0) <= 0.08726646259971647))))

Network N:
Input_0 : Input([ -1 200 200 1], dtype=float32)
Transpose_0 : Transpose(Input_0, permutation=[0 3 1 2])
Conv_0 : Conv(Transpose_0, out_channels=32, kernel_shape=[5, 5], strides=[2, 2], pads=[1, 1, 2, 2], group=1, dilations=[1, 1])
MaxPool_0 : MaxPool(Conv_0)
Identity_0 : Identity(MaxPool_0)
Conv_1 : Conv(Identity_0, out_channels=32, kernel_shape=[1, 1], strides=[2, 2], pads=[0, 0, 0, 0], group=1, dilations=[1, 1])
BatchNormalization_0 : BatchNormalization(Identity_0)
Relu_0 : Relu(BatchNormalization_0)
Conv_2 : Conv(Relu_0, out_channels=32, kernel_shape=[3, 3], strides=[2, 2], pads=[1, 1, 1, 1], group=1, dilations=[1, 1])
BatchNormalization_1 : BatchNormalization(Conv_2)
Relu_1 : Relu(BatchNormalization_1)
Conv_3 : Conv(Relu_1, out_channels=32, kernel_shape=[3, 3], strides=[1, 1], pads=[1, 1, 1, 1], group=1, dilations=[1, 1])
Add_0 : Add(Conv_1, Conv_3)
Conv_4 : Conv(Add_0, out_channels=64, kernel_shape=[1, 1], strides=[2, 2], pads=[0, 0, 0, 0], group=1, dilations=[1, 1])
BatchNormalization_2 : BatchNormalization(Add_0)
Relu_2 : Relu(BatchNormalization_2)
Conv_5 : Conv(Relu_2, out_channels=64, kernel_shape=[3, 3], strides=[2, 2], pads=[1, 1, 1, 1], group=1, dilations=[1, 1])
BatchNormalization_3 : BatchNormalization(Conv_5)
Relu_3 : Relu(BatchNormalization_3)
Conv_6 : Conv(Relu_3, out_channels=64, kernel_shape=[3, 3], strides=[1, 1], pads=[1, 1, 1, 1], group=1, dilations=[1, 1])
Add_1 : Add(Conv_4, Conv_6)
Conv_7 : Conv(Add_1, out_channels=128, kernel_shape=[1, 1], strides=[2, 2], pads=[0, 0, 0, 0], group=1, dilations=[1, 1])
BatchNormalization_4 : BatchNormalization(Add_1)
Relu_4 : Relu(BatchNormalization_4)
Conv_8 : Conv(Relu_4, out_channels=128, kernel_shape=[3, 3], strides=[2, 2], pads=[1, 1, 1, 1], group=1, dilations=[1, 1])
BatchNormalization_5 : BatchNormalization(Conv_8)
Relu_5 : Relu(BatchNormalization_5)
Conv_9 : Conv(Relu_5, out_channels=128, kernel_shape=[3, 3], strides=[1, 1], pads=[1, 1, 1, 1], group=1, dilations=[1, 1])
Add_2 : Add(Conv_7, Conv_9)
Transpose_1 : Transpose(Add_2, permutation=[0 2 3 1])
Flatten_0 : Flatten(Transpose_1, axis=1)
Relu_6 : Relu(Flatten_0)
Identity_1 : Identity(Relu_6)
MatMul_0 : MatMul(Identity_1, ndarray(shape=(6272, 1)))
Add_3 : Add(MatMul_0, [0.01033337])
Identity_2 : Identity(Add_3)
MatMul_1 : MatMul(Identity_1, ndarray(shape=(6272, 1)))
Add_4 : Add(MatMul_1, [1.1624445])
Sigmoid_0 : Sigmoid(Add_4)
Identity_3 : Identity(Sigmoid_0)
Concat_0 : Concat(['Identity_2', 'Identity_3'])

2022-10-24 11:48:55.000739: I tensorflow/core/platform/cpu_feature_guard.cc:151] This TensorFlow binary is optimized with oneAPI Deep Neural Network Library (oneDNN) to use the following CPU instructions in performance-critical operations: AVX2 AVX512F FMA
To enable them in other operations, rebuild TensorFlow with the appropriate compiler flags.
2022-10-24 11:48:57.642840: I tensorflow/core/common_runtime/gpu/gpu_device.cc:1525] Created device /job:localhost/replica:0/task:0/device:GPU:0 with 5222 MB memory: -> device: 0, name: NVIDIA GeForce GTX 1080 Ti, pci bus id: 0000:3b:00.0, compute capability: 6.1
2022-10-24 11:48:57.644271: I tensorflow/core/common_runtime/gpu/gpu_device.cc:1525] Created device /job:localhost/replica:0/task:0/device:GPU:1 with 7072 MB memory: -> device: 1, name: NVIDIA GeForce GTX 1080 Ti, pci bus id: 0000:5e:00.0, compute capability: 6.1
2022-10-24 11:48:57.646563: I tensorflow/core/common_runtime/gpu/gpu_device.cc:1525] Created device /job:localhost/replica:0/task:0/device:GPU:2 with 7096 MB memory: -> device: 2, name: NVIDIA GeForce GTX 1080 Ti, pci bus id: 0000:86:00.0, compute capability: 6.1
2022-10-24 11:48:57.649086: I tensorflow/core/common_runtime/gpu/gpu_device.cc:1525] Created device /job:localhost/replica:0/task:0/device:GPU:3 with 7045 MB memory: -> device: 3, name: NVIDIA GeForce GTX 1080 Ti, pci bus id: 0000:af:00.0, compute capability: 6.1
2022-10-24 11:48:58.140240: I tensorflow/stream_executor/cuda/cuda_dnn.cc:366] Loaded cuDNN version 8201
2022-10-24 11:49:00.473526: E tensorflow/stream_executor/cuda/cuda_blas.cc:197] failed to set new cublas math mode: CUBLAS_STATUS_INVALID_VALUE
2022-10-24 11:49:00.473600: W tensorflow/core/framework/op_kernel.cc:1745] OP_REQUIRES failed at matmul_op_impl.h:442 : INTERNAL: Failed initializing math mode
Traceback (most recent call last):
File "/media/sdc1/shenw/sandbox/nn_assurance/dnnf/.venv/lib/python3.8/site-packages/dnnv/nn/converters/tensorflow.py", line 58, in wrapped_func
self._cache[func] = func(*args, **kwargs)
File "/media/sdc1/shenw/sandbox/nn_assurance/dnnf/.venv/lib/python3.8/site-packages/dnnv/nn/converters/tensorflow.py", line 588, in matmul_func
result = tf.matmul(a, b)

It looks like there is error in
failed to set new cublas math mode: CUBLAS_STATUS_INVALID_VALUE

So I searched the Internet for the solution to this error. And found the following site
tensorflow/tensorflow#57359

A solution is suggested that adding the following line to python code would fix the problem.
tf.config.experimental.enable_tensor_float_32_execution(False)

However I could not locate the tensorflow code in your dnnf codebase, and hence can't add the above line to your code.
Cold you point me to where I could add the line of
tf.config.experimental.enable_tensor_float_32_execution(False)
to fix the error?

Your help will be greatly appreciated. Thanks!

dnnf_ghpr_benchmark_error.txt