Some of the 2.0 folder have vnnlib 1.0 syntax (no version or network, flat inputs)
For example safenlp (link): starts with:
; medical perturbations property.
(declare-const X_0 Real)
(declare-const X_1 Real)
Also CORA (link) [it looks like 20 of them were converted, others remain 1.0]:
; cifar10-img205.vnnlib
; Declare the input variables.
(declare-const X_0 Real)
(declare-const X_1 Real)
Also others (some examples):
- malbeware (malbeware/2.0/vnnlib/malbeware_family-Adialer.C_label-0_eps-2_idx-4.vnnlib)
- linearizenn linearizenn_2024/2.0/vnnlib/prop_10_10_0_io.vnnlib
- cersyve cersyve2.0/vnnlib/prop_cart_pole.vnnlib
linearize_nn 1.0 the _io instances like prop_120_120_0_io have (<= (a b)) style comparisons (should be (<= a b). for example:
(assert (or
(and (<= (3.73754957079315 (- Y_0 (+ (* 18.401223410915446 X_2) (* 11.99967493121423 X_3) -41.19699414025808)))))
(and (>= (-1.6096789719826952 (- Y_0 (+ (* 18.401223410915446 X_2) (* 11.99967493121423 X_3) -41.19699414025808)))))
))
monotonic acas xu (I think this was mentioned in another issue) has infix asserts (benchmarks/monotonic_acasxu_2026/2.0/vnnlib/instance_0.vnnlib):
(assert (Y_f[3] < Y_g[3])) instead of (assert (< Y_f[3] Y_g[3]))
isomorphic acas xu has trivially unsat output constraints (likely an and where an or was intended) benchmarks/isomorphic_acasxu_2026/2.0/vnnlib/instance_0.vnnlib :
(assert (and (> Y_g[0] (+ Y_f[0] 0.05)) (< Y_g[0] (- Y_f[0] 0.05))))
cgan_2023: when cGAN_imgSz32_nCh_3_small_transformer.onnx is downloaded by the large models download, it doesn't get placed in the 1.0/onnx or the 2.0/onnx folder... instead it makes an onnx folder at one directory higher, so it's not in the same location as the other onnx files for this benchmark. Not sure if this was intentional.
Some of the 2.0 folder have vnnlib 1.0 syntax (no version or network, flat inputs)
For example safenlp (link): starts with:
Also CORA (link) [it looks like 20 of them were converted, others remain 1.0]:
Also others (some examples):
linearize_nn 1.0 the _io instances like prop_120_120_0_io have
(<= (a b))style comparisons (should be(<= a b). for example:monotonic acas xu (I think this was mentioned in another issue) has infix asserts (benchmarks/monotonic_acasxu_2026/2.0/vnnlib/instance_0.vnnlib):
(assert (Y_f[3] < Y_g[3]))instead of(assert (< Y_f[3] Y_g[3]))isomorphic acas xu has trivially unsat output constraints (likely an
andwhere anorwas intended) benchmarks/isomorphic_acasxu_2026/2.0/vnnlib/instance_0.vnnlib :(assert (and (> Y_g[0] (+ Y_f[0] 0.05)) (< Y_g[0] (- Y_f[0] 0.05))))cgan_2023: when cGAN_imgSz32_nCh_3_small_transformer.onnx is downloaded by the large models download, it doesn't get placed in the 1.0/onnx or the 2.0/onnx folder... instead it makes an onnx folder at one directory higher, so it's not in the same location as the other onnx files for this benchmark. Not sure if this was intentional.