diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h index d6fbca6728a..71ef9f4d6b4 100644 --- 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 index 21b21908943..e7c250481eb 100644 --- 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 index 46a9b7c8709..76895155ad4 100644 --- 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)