fix folder name (date)

non-incremental/UFDTLIA/2026-04-28-Grounders/PackingProblem.smt2

@@ -0,0 +1,82 @@
+
+(set-info :smt-lib-version 2.6)
+(set-logic UFDTLIA)
+(set-info :source |
+Generated by: Pierre Carbonnelle
+Generated on: 2026-04-28
+Generator: https://github.com/xmt-lib/benchmarks
+Application: industrial configuration problem
+Target solver: Z3
+Publications: https://arxiv.org/abs/2602.19102
+Time limit: 300
+From the DIRT benchmark used to evaluate grounders
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "random")
+(set-info :status sat)
+
+(declare-datatype Square ( (q1) (q2) (q3) (q4) (q5) (q6) (q7) (q8) (q9) (q10) (q11) (q12) (q13) (q14) (q15) (q16) (q17) (q18) (q19) (q20) (q21) (q22) (q23) (q24) (q25) (q26) (q27) (q28) (q29) (q30) (q31) ))
+
+(declare-fun pos_x (Square) Int)
+(declare-fun pos_y (Square) Int)
+(declare-fun square_size (Square) Int)
+
+(assert (= (square_size q1) 88))
+(assert (= (square_size q2) 106))
+(assert (= (square_size q3) 37))
+(assert (= (square_size q4) 47))
+(assert (= (square_size q5) 57))
+(assert (= (square_size q6) 145))
+(assert (= (square_size q7) 9))
+(assert (= (square_size q8) 28))
+(assert (= (square_size q9) 9))
+(assert (= (square_size q10) 10))
+(assert (= (square_size q11) 24))
+(assert (= (square_size q12) 23))
+(assert (= (square_size q13) 16))
+(assert (= (square_size q14) 47))
+(assert (= (square_size q15) 23))
+(assert (= (square_size q16) 24))
+(assert (= (square_size q17) 27))
+(assert (= (square_size q18) 22))
+(assert (= (square_size q19) 42))
+(assert (= (square_size q20) 13))
+(assert (= (square_size q21) 6))
+(assert (= (square_size q22) 8))
+(assert (= (square_size q23) 46))
+(assert (= (square_size q24) 25))
+(assert (= (square_size q25) 8))
+(assert (= (square_size q26) 14))
+(assert (= (square_size q27) 45))
+(assert (= (square_size q28) 45))
+(assert (= (square_size q29) 5))
+(assert (= (square_size q30) 42))
+(assert (= (square_size q31) 37))
+
+(declare-fun area_width () Int)
+(declare-fun area_height () Int)
+
+(assert (forall ((s Square)) (<= 0 (pos_x s))))
+(assert (forall ((s Square)) (<= 0 (pos_y s))))
+(assert (forall ((s Square)) (<= (+ (pos_x s) (square_size s)) area_width)))
+(assert (forall ((s Square)) (<= (+ (pos_y s) (square_size s)) area_height)))
+
+(assert (forall ((s1 Square) (s2 Square))
+                (not (and (not (= s1 s2))
+
+                          (<= (pos_x s1) (pos_x s2))
+                          (<= (pos_y s1) (pos_y s2))
+
+                          (< (pos_x s2) (+ (pos_x s1) (square_size s1)))
+                          (< (pos_x s1) (+ (pos_x s2) (square_size s2)))
+                          (< (pos_y s2) (+ (pos_y s1) (square_size s1)))
+                          (< (pos_y s1) (+ (pos_y s2) (square_size s2)))
+
+                          (<= (+ (pos_x s2) (square_size s2)) (+ (pos_x s1) (square_size s1)))
+                          (<= (+ (pos_y s2) (square_size s2)) (+ (pos_y s1) (square_size s1)))
+                     )
+              )))
+(assert (= area_width  300))
+(assert (= area_height 250))
+
+(check-sat)