More

ajreynol · Nov 16, 2024 · 85c3ea4 · 85c3ea4
1 parent 6d2262c
commit 85c3ea4
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 5 deletions.
diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h
@@ -3570,6 +3570,8 @@ enum ENUM(ProofRewriteRule)
   EVALUE(STR_EQ_CTN_FULL_FALSE1),
   /** Auto-generated from RARE rule str-eq-ctn-full-false2 */
   EVALUE(STR_EQ_CTN_FULL_FALSE2),
+  /** Auto-generated from RARE rule str-eq-len-false */
+  EVALUE(STR_EQ_LEN_FALSE),
   /** Auto-generated from RARE rule str-concat-flatten */
   EVALUE(STR_CONCAT_FLATTEN),
   /** Auto-generated from RARE rule str-concat-flatten-eq */

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
@@ -275,7 +275,7 @@ name   = "SMT Layer"
 
 [[option]]
   name       = "extRewPrep"
-  category   = "regular"
+  category   = "expert"
   long       = "ext-rew-prep=MODE"
   type       = "ExtRewPrepMode"
   default    = "OFF"

diff --git a/src/theory/strings/rewrites b/src/theory/strings/rewrites
@@ -22,10 +22,10 @@
   (= x y)
   false)
 
-;(define-cond-rule str-eq-len-false ((x String) (y String))
-;  (not (= (str.len x) (str.len y)))
-;  (= x y)
-;  false)
+(define-cond-rule str-eq-len-false ((x String) (y String))
+  (not (= (str.len x) (str.len y)))
+  (= x y)
+  false)
 
 (define-rule str-concat-flatten ((xs ?Seq :list) (s ?Seq) (ys ?Seq :list) (zs ?Seq :list))
   (str.++ xs (str.++ s ys) zs)