.

Veridise · Aug 31, 2023 · 5c165af · 5c165af
1 parent 960dae6
commit 5c165af
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/picus/algorithms/lemmas/linear-lemma.rkt b/picus/algorithms/lemmas/linear-lemma.rkt
@@ -41,12 +41,12 @@
   (define res (make-hash))
   (for ([clause (in-list linear-clauses)])
     (match-define (cons deducible-vars nonlinear-vars) clause)
+    ;; NOTE(sorawee): I think this is not optimal. We should revisit this.
     (define len-deducible (set-count deducible-vars))
-    (define len-nonlinear (set-count nonlinear-vars))
     (for ([var (in-set deducible-vars)])
-      (hash-update! res var (λ (old) (max old (exact->inexact (/ 1 (+ len-deducible len-nonlinear))))) 0))
+      (hash-update! res var (λ (old) (+ old len-deducible -1)) 0))
     (for ([var (in-set nonlinear-vars)])
-      (hash-update! res var (λ (old) (max old (exact->inexact (/ 1 (+ len-deducible len-nonlinear))))) 0)))
+      (hash-update! res var (λ (old) (+ old len-deducible)) 0)))
   res)
 
 ; recursively apply linear lemma

diff --git a/tests/circomlib-test.rkt b/tests/circomlib-test.rkt
@@ -20,7 +20,7 @@
       (parameterize ([current-namespace (make-base-namespace)]
                      [current-command-line-arguments
                       (vector "--solver" "cvc5"
-                              "--timeout" "5000"
+                              "--timeout" "10000"
                               "--weak"
                               "--verbose" "1"
                               "--r1cs"