diff --git a/picus/optimizers/r1cs-cvc5-simple-optimizer.rkt b/picus/optimizers/r1cs-cvc5-simple-optimizer.rkt
index 8eba505..e8ab8c7 100644
--- a/picus/optimizers/r1cs-cvc5-simple-optimizer.rkt
+++ b/picus/optimizers/r1cs-cvc5-simple-optimizer.rkt
@@ -156,15 +156,15 @@
             (cond
                 ; replace as p
                 [(= config:p v) (r1cs:rvar "p")]
-                [(= (- config:p 1) v) (r1cs:rvar "ps1")]
-                [(= (- config:p 2) v) (r1cs:rvar "ps2")]
-                [(= (- config:p 3) v) (r1cs:rvar "ps3")]
-                [(= (- config:p 4) v) (r1cs:rvar "ps4")]
-                [(= (- config:p 5) v) (r1cs:rvar "ps5")]
+                ;[(= (- config:p 1) v) (r1cs:rvar "ps1")]
+                ;[(= (- config:p 2) v) (r1cs:rvar "ps2")]
+                ;[(= (- config:p 3) v) (r1cs:rvar "ps3")]
+                ;[(= (- config:p 4) v) (r1cs:rvar "ps4")]
+                ;[(= (- config:p 5) v) (r1cs:rvar "ps5")]
                 ; replace as zero
-                [(= 0 v) (r1cs:rvar "zero")]
+                ;[(= 0 v) (r1cs:rvar "zero")]
                 ; replace as one
-                [(= 1 v) (r1cs:rvar "one")]
+                ;[(= 1 v) (r1cs:rvar "one")]
                 ; do nothing
                 [else (r1cs:rint v)]
             )
diff --git a/test-pp-uniqueness.rkt b/test-pp-uniqueness.rkt
index 89e755d..6bb7881 100644
--- a/test-pp-uniqueness.rkt
+++ b/test-pp-uniqueness.rkt
@@ -34,6 +34,7 @@
 (define arg-solver "z3")
 (define arg-timeout 5000)
 (define arg-smt #f)
+(define arg-weak #f)
 (command-line
     #:once-each
     [("--r1cs") p-r1cs "path to target r1cs"
@@ -60,11 +61,17 @@
             (set! arg-smt #t)
         )
     ]
+    [("--weak") "only check weak safety, not strong safety  (default: false)"
+        (begin
+            (set! arg-weak #t)
+        )
+    ]
 )
 (printf "# r1cs file: ~a\n" arg-r1cs)
 (printf "# timeout: ~a\n" arg-timeout)
 (printf "# solver: ~a\n" arg-solver)
 
+
 ; =========================================
 ; ======== solver specific methods ========
 ; =========================================
@@ -371,7 +378,13 @@
             )
             (if (null? ukn)
                 null
-                (apply-complete-iteration kn ukn c2ukn (list-ref signal2constraints signal-smt) new-failures)
+                (if arg-weak
+                    (if (utils:empty_inter? ukn output-list)
+                        ukn
+                        (apply-complete-iteration kn ukn c2ukn (list-ref signal2constraints signal-smt) new-failures)
+                    )
+                    (apply-complete-iteration kn ukn c2ukn (list-ref signal2constraints signal-smt) new-failures)
+                )
             )
         ]
         [else ukn]
@@ -468,9 +481,12 @@
 
 (define res-ul (apply-complete-iteration known-list unknown-list initial-constraint2ukn (range mconstraints) '()))
 (printf "# final unknown list: ~a\n" res-ul)
-(if (empty? res-ul)
-    (printf "# Strong safety verified.\n")
-    (printf "# Strong safey failed.\n")
+(if (not arg-weak)
+    (if (empty? res-ul)
+        (printf "# Strong safety verified.\n")
+        (printf "# Strong safey failed.\n")
+    )
+    (printf "# Weak flag activated: skipping check strong safey\n")
 )
 
 (if (utils:empty_inter? res-ul output-list)