Exception occured during execution

[habeebp098]

I am getting the following error message while running the nnenum tool.

_all input names: ['W0', 'X', 'M0', 'B0', 'H0', 'W1', 'R0', 'M1', 'B1', 'H1', 'W2', 'R1', 'M2', 'B2', 'H2', 'W3', 'R2', 'M3', 'B3', 'H3', 'W4', 'R3', 'M4', 'B4', 'H4', 'W5', 'R4', 'M5', 'B5', 'H5', 'W6', 'R5', 'M6', 'B6']
Running in parallel with 8 processes
(0.6 sec) Q: 0, Sets: 0/1 (0.0%) ETA: - (expected 1 stars)
(0.7 sec) Q: 16, Sets: 0/28 (0.0%) ETA: - (expected 1 stars)
Note: minimize failed with fail_on_unsat was true, trying to reset basis...
still unsat after reset basis, trying no-dir optimization
Error: No-dir result was also infeasible!
Lp has 5 columns (variables) and 15 rows (constraints)
*i0 *i1 *i2 *i3 i4
min 0.0000 0.0000 0.0000 0.0000 0.0000
subject to:
BS BS BS NL BS
1: BS 0.1037 -0.165 -0.006 0.6373 -0.745 <= 0.1143
2: BS 0.1037 -0.165 -0.006 0.6373 -0.745 <= 0.1143
3: NU -0.096 -0.625 0.6884 -0.170 0.3101 <= 0.1591
4: BS 0.0961 0.6258 -0.688 0.1701 -0.310 <= -0.159
5: BS -0.071 -0.088 0.1373 -0.871 0.4571 <= 0.3537
6: BS -0.071 -0.088 0.1373 -0.871 0.4571 <= 0.3537
7: BS -0.044 -0.958 -0.062 -0.200 0.1890 <= 0.0130
8: BS -0.044 -0.958 -0.062 -0.200 0.1890 <= 0.0130
9: NU -0.014 -0.871 -0.320 0.3490 -0.123 <= 0.2251
10: BS -0.014 -0.871 -0.320 0.3490 -0.123 <= 0.2251
11: BS -0.107 -0.793 0.0031 -0.389 0.4543 <= -0.178
12: BS -0.001 -0.194 -0.976 -0.073 0.0565 <= 0.2362
13: NU -0.008 0.1193 0.9912 0.0517 -0.021 <= -0.206
14: NU 0.2230 -0.348 -0.777 -0.320 -0.347 <= -0.514
15: BS -0.179 0.7511 0.4135 0.4458 0.1833 <= 0.4529
() Bounded variables:
i0 in [0.0, 60760.0]
i1 in [-3.1415929794311523, 3.1415929794311523]
i2 in [-3.1415929794311523, 3.1415929794311523]
i3 in [100.0, 1200.0]
i4 in [0.0, 1200.0]

Traceback (most recent call last):
File "/home/habeeb/nnenum/nnenum-master/src/nnenum/enumerate.py", line 486, in worker_func
w.main_loop()
File "/home/habeeb/nnenum/nnenum-master/src/nnenum/worker.py", line 67, in main_loop
self.advance_star()
File "/home/habeeb/nnenum/nnenum-master/src/nnenum/worker.py", line 827, in advance_star
new_star = ss.do_first_relu_split(network, spec, self.priv.start_time)
File "/home/habeeb/nnenum/nnenum-master/src/nnenum/lp_star_state.py", line 307, in do_first_relu_split
rv = self.split_enumerate(index, network, spec, start_time)
File "/home/habeeb/nnenum/nnenum-master/src/nnenum/lp_star_state.py", line 280, in split_enumerate
child.prefilter = self.prefilter.split_relu(i, pos.star, neg.star, self_gets_positive, start_time, depth)
File "/home/habeeb/nnenum/nnenum-master/src/nnenum/prefilter.py", line 317, in split_relu
neg.zono.contract_lp(neg_star, row, -bias)
File "/home/habeeb/nnenum/nnenum-master/src/nnenum/zonotope.py", line 123, in contract_lp
new_bounds_list = star.update_input_box_bounds(hyperplane_vec, rhs, count_lps=True)
File "/home/habeeb/nnenum/nnenum-master/src/nnenum/lp_star.py", line 272, in update_input_box_bounds
rv = self.update_input_box_bounds_new(cur_box, should_skip, count_lps)
File "/home/habeeb/nnenum/nnenum-master/src/nnenum/lp_star.py", line 305, in update_input_box_bounds_new
res = self.lpi.minimize(vec)
File "/home/habeeb/nnenum/nnenum-master/src/nnenum/lpinstance.py", line 730, in minimize
raise UnsatError("minimize returned UNSAT and fail_on_unsat was True")
nnenum.lpinstance.UnsatError: minimize returned UNSAT and fail_on_unsat was True

Worker 2 had exception
Worker 2 quitting due to exception in some worker
Worker 4 quitting due to exception in some worker
Worker 4 quitting due to exception in some worker
Worker 3 quitting due to exception in some worker
Worker 3 quitting due to exception in some worker
Worker 5 quitting due to exception in some worker
Worker 5 quitting due to exception in some worker
Worker 6 quitting due to exception in some worker
Worker 6 quitting due to exception in some worker
Worker 1 quitting due to exception in some worker
Worker 1 quitting due to exception in some worker
Worker 7 quitting due to exception in some worker
Worker 7 quitting due to exception in some worker
Worker 0 quitting due to exception in some worker
Worker 0 quitting due to exception in some worker

Exception occured during execution_

Attached are the network and the property files.

net.txt
p2_acaxurange.vnnlib.txt

[stanleybak]

I upgraded the version of packages like numpy, scipy and glpk before working on this, and now the bug seems to be gone. @habeebp098 can you confirm this is fixed using the latest version in master?

[habeebp098]

The error still exists.

If I run the tool with the output constraint Y_0 - Y_5 <= -0.0001, for the network net.onnx.txt, the tool throws an exception.

prop_1.vnnlib.txt

Thanks