From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 6 May 2021 21:57:37 +0000 (-0500)
Subject: Discard duplicate terms in patterns (#6501)
X-Git-Tag: cvc5-1.0.0~1787
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d0c3c164c9f722d4ea506706c5843373c8a948c4;p=cvc5.git

Discard duplicate terms in patterns (#6501)

Fixes #6495.
---

diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
index 193ba250e..a937edf44 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
@@ -146,6 +146,11 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat)
   std::vector<Node> nodes;
   for (const Node& p : pat)
   {
+    if (std::find(nodes.begin(), nodes.end(), p) != nodes.end())
+    {
+      // skip duplicate pattern term
+      continue;
+    }
     Node pat_use = PatternTermSelector::getIsUsableTrigger(p, q);
     if (pat_use.isNull())
     {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3f1ff1307..a64a1eb1e 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2383,6 +2383,7 @@ set(regress_2_tests
   regress2/instance_1444.smtv1.smt2
   regress2/issue3687-check-models.smt2
   regress2/issue4707-bv-to-bool-large.smt2
+  regress2/issue6495-dup-pat-term.smt2
   regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2
   regress2/javafe.ast.WhileStmt.447_no_forall.smt2
   regress2/nl/nt-lemmas-bad.smt2
diff --git a/test/regress/regress2/issue6495-dup-pat-term.smt2 b/test/regress/regress2/issue6495-dup-pat-term.smt2
new file mode 100644
index 000000000..3c8d0df61
--- /dev/null
+++ b/test/regress/regress2/issue6495-dup-pat-term.smt2
@@ -0,0 +1,298 @@
+; COMMAND-LINE: -i -q
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-sort |T@[Int]Int| 0)
+(declare-datatypes ((T@Vec_2846 0)) (((Vec_2846 (|v#Vec_2846| |T@[Int]Int|) (|l#Vec_2846| Int) ) ) ))
+(declare-datatypes ((T@$Location 0)) ((($Global (|a#$Global| Int) ) ($Local (|i#$Local| Int) ) ($Param (|i#$Param| Int) ) ) ))
+(declare-datatypes ((T@$Path 0)) ((($Path (|p#$Path| |T@[Int]Int|) (|size#$Path| Int) ) ) ))
+(declare-datatypes ((T@$Mutation_3470 0)) ((($Mutation_3470 (|l#$Mutation_3470| T@$Location) (|p#$Mutation_3470| T@$Path) (|v#$Mutation_3470| Int) ) ) ))
+(declare-datatypes ((T@$Mutation_8806 0)) ((($Mutation_8806 (|l#$Mutation_8806| T@$Location) (|p#$Mutation_8806| T@$Path) (|v#$Mutation_8806| T@Vec_2846) ) ) ))
+(declare-datatypes ((T@$Range 0)) ((($Range (|lb#$Range| Int) (|ub#$Range| Int) ) ) ))
+(declare-fun $MAX_U8 () Int)
+(declare-fun $MAX_U64 () Int)
+(declare-fun $MAX_U128 () Int)
+(declare-fun |$IsValid'u8'| (Int) Bool)
+(declare-fun |$IsValid'u64'| (Int) Bool)
+(declare-fun |$IsValid'u128'| (Int) Bool)
+(declare-fun |$IsValid'num'| (Int) Bool)
+(declare-fun |$IsValid'address'| (Int) Bool)
+(declare-fun $InRange (T@$Range Int) Bool)
+(declare-fun $EmptyPath () T@$Path)
+(declare-sort |T@[Int]Bool| 0)
+(declare-fun $ConstMemoryDomain (Bool) |T@[Int]Bool|)
+(declare-fun |lambda#0| (Bool) |T@[Int]Bool|)
+(declare-fun $EXEC_FAILURE_CODE () Int)
+(declare-fun $shl (Int Int) Int)
+(declare-fun $shr (Int Int) Int)
+(declare-fun |$IsEqual'vec'u64''| (T@Vec_2846 T@Vec_2846) Bool)
+(declare-fun InRangeVec_2846 (T@Vec_2846 Int) Bool)
+(declare-fun |Select__T@[Int]Int_| (|T@[Int]Int| Int) Int)
+(declare-fun |$IsValid'vec'u64''| (T@Vec_2846) Bool)
+(declare-fun |$IndexOfVec'u64'| (T@Vec_2846 Int) Int)
+(declare-fun |$IsEqual'vec'u8''| (T@Vec_2846 T@Vec_2846) Bool)
+(declare-fun |$IsValid'vec'u8''| (T@Vec_2846) Bool)
+(declare-fun |$IndexOfVec'u8'| (T@Vec_2846 Int) Int)
+(declare-fun $Hash_sha2 (T@Vec_2846) T@Vec_2846)
+(declare-fun $Hash_sha3 (T@Vec_2846) T@Vec_2846)
+(declare-fun $Signature_$ed25519_validate_pubkey (T@Vec_2846) Bool)
+(declare-fun $Signature_$ed25519_verify (T@Vec_2846 T@Vec_2846 T@Vec_2846) Bool)
+(declare-fun IndexOfVec_2846 (T@Vec_2846 Int) Int)
+(declare-fun |Select__T@[Int]Bool_| (|T@[Int]Bool| Int) Bool)
+(declare-fun |lambda#2| (Int Int Int |T@[Int]Int| |T@[Int]Int| Int Int) |T@[Int]Int|)
+(declare-fun |lambda#3| (Int Int |T@[Int]Int| Int Int Int) |T@[Int]Int|)
+(declare-fun |lambda#4| (Int Int Int |T@[Int]Int| |T@[Int]Int| Int Int) |T@[Int]Int|)
+(assert (= $MAX_U8 255))
+(assert (= $MAX_U64 18446744073709551615))
+(assert (= $MAX_U128 340282366920938463463374607431768211455))
+(assert (forall ((v Int) ) (! (= (|$IsValid'u8'| v)  (and (>= v 0) (<= v $MAX_U8)))
+ :qid |outputbpl.190:23|
+ :skolemid |6|
+ :pattern ( (|$IsValid'u8'| v))
+)))
+(assert (forall ((v@@0 Int) ) (! (= (|$IsValid'u64'| v@@0)  (and (>= v@@0 0) (<= v@@0 $MAX_U64)))
+ :qid |outputbpl.194:24|
+ :skolemid |7|
+ :pattern ( (|$IsValid'u64'| v@@0))
+)))
+(assert (forall ((v@@1 Int) ) (! (= (|$IsValid'u128'| v@@1)  (and (>= v@@1 0) (<= v@@1 $MAX_U128)))
+ :qid |outputbpl.198:25|
+ :skolemid |8|
+ :pattern ( (|$IsValid'u128'| v@@1))
+)))
+(assert (forall ((v@@2 Int) ) (! (= (|$IsValid'num'| v@@2) true)
+ :qid |outputbpl.202:24|
+ :skolemid |9|
+ :pattern ( (|$IsValid'num'| v@@2))
+)))
+(assert (forall ((v@@3 Int) ) (! (= (|$IsValid'address'| v@@3) (>= v@@3 0))
+ :qid |outputbpl.206:28|
+ :skolemid |10|
+ :pattern ( (|$IsValid'address'| v@@3))
+)))
+(assert (forall ((r T@$Range) (i Int) ) (! (= ($InRange r i)  (and (<= (|lb#$Range| r) i) (< i (|ub#$Range| r))))
+ :qid |outputbpl.216:19|
+ :skolemid |11|
+ :pattern ( ($InRange r i))
+)))
+(assert (= (|size#$Path| $EmptyPath) 0))
+(assert (= ($ConstMemoryDomain false) (|lambda#0| false)))
+(assert (= ($ConstMemoryDomain true) (|lambda#0| true)))
+(assert (= $EXEC_FAILURE_CODE (- 0 1)))
+(assert (forall ((src1 Int) (p Int) ) (! (= ($shl src1 p) (ite (= p 8) (* src1 256) (ite (= p 16) (* src1 65536) (ite (= p 32) (* src1 4294967296) (ite (= p 64) (* src1 18446744073709551616) (- 0 1))))))
+ :qid |outputbpl.469:15|
+ :skolemid |12|
+ :pattern ( ($shl src1 p))
+)))
+(assert (forall ((src1@@0 Int) (p@@0 Int) ) (! (= ($shr src1@@0 p@@0) (ite (= p@@0 8) (div src1@@0 256) (ite (= p@@0 16) (div src1@@0 65536) (ite (= p@@0 32) (div src1@@0 4294967296) (ite (= p@@0 64) (div src1@@0 18446744073709551616) (- 0 1))))))
+ :qid |outputbpl.478:15|
+ :skolemid |13|
+ :pattern ( ($shr src1@@0 p@@0))
+)))
+(assert (forall ((v1 T@Vec_2846) (v2 T@Vec_2846) ) (! (= (|$IsEqual'vec'u64''| v1 v2)  (and (= (|l#Vec_2846| v1) (|l#Vec_2846| v2)) (forall ((i@@0 Int) ) (!  (=> (InRangeVec_2846 v1 i@@0) (= (|Select__T@[Int]Int_| (|v#Vec_2846| v1) i@@0) (|Select__T@[Int]Int_| (|v#Vec_2846| v2) i@@0)))
+ :qid |outputbpl.602:13|
+ :skolemid |14|
+))))
+ :qid |outputbpl.600:29|
+ :skolemid |15|
+ :pattern ( (|$IsEqual'vec'u64''| v1 v2))
+)))
+(assert (forall ((v@@4 T@Vec_2846) ) (! (= (|$IsValid'vec'u64''| v@@4)  (and (|$IsValid'u64'| (|l#Vec_2846| v@@4)) (forall ((i@@1 Int) ) (!  (=> (InRangeVec_2846 v@@4 i@@1) (|$IsValid'u64'| (|Select__T@[Int]Int_| (|v#Vec_2846| v@@4) i@@1)))
+ :qid |outputbpl.608:13|
+ :skolemid |16|
+))))
+ :qid |outputbpl.606:29|
+ :skolemid |17|
+ :pattern ( (|$IsValid'vec'u64''| v@@4))
+)))
+(assert (forall ((v@@5 T@Vec_2846) (e Int) ) (! (let ((i@@2 (|$IndexOfVec'u64'| v@@5 e)))
+(ite  (not (exists ((i@@3 Int) ) (!  (and (and (|$IsValid'u64'| i@@3) (InRangeVec_2846 v@@5 i@@3)) (= (|Select__T@[Int]Int_| (|v#Vec_2846| v@@5) i@@3) e))
+ :qid |outputbpl.613:13|
+ :skolemid |18|
+))) (= i@@2 (- 0 1))  (and (and (and (|$IsValid'u64'| i@@2) (InRangeVec_2846 v@@5 i@@2)) (= (|Select__T@[Int]Int_| (|v#Vec_2846| v@@5) i@@2) e)) (forall ((j Int) ) (!  (=> (and (and (|$IsValid'u64'| j) (>= j 0)) (< j i@@2)) (not (= (|Select__T@[Int]Int_| (|v#Vec_2846| v@@5) j) e)))
+ :qid |outputbpl.621:17|
+ :skolemid |19|
+)))))
+ :qid |outputbpl.617:15|
+ :skolemid |20|
+ :pattern ( (|$IndexOfVec'u64'| v@@5 e))
+)))
+(assert (forall ((v1@@0 T@Vec_2846) (v2@@0 T@Vec_2846) ) (! (= (|$IsEqual'vec'u8''| v1@@0 v2@@0)  (and (= (|l#Vec_2846| v1@@0) (|l#Vec_2846| v2@@0)) (forall ((i@@4 Int) ) (!  (=> (InRangeVec_2846 v1@@0 i@@4) (= (|Select__T@[Int]Int_| (|v#Vec_2846| v1@@0) i@@4) (|Select__T@[Int]Int_| (|v#Vec_2846| v2@@0) i@@4)))
+ :qid |outputbpl.789:13|
+ :skolemid |21|
+))))
+ :qid |outputbpl.787:28|
+ :skolemid |22|
+ :pattern ( (|$IsEqual'vec'u8''| v1@@0 v2@@0))
+)))
+(assert (forall ((v@@6 T@Vec_2846) ) (! (= (|$IsValid'vec'u8''| v@@6)  (and (|$IsValid'u64'| (|l#Vec_2846| v@@6)) (forall ((i@@5 Int) ) (!  (=> (InRangeVec_2846 v@@6 i@@5) (|$IsValid'u8'| (|Select__T@[Int]Int_| (|v#Vec_2846| v@@6) i@@5)))
+ :qid |outputbpl.795:13|
+ :skolemid |23|
+))))
+ :qid |outputbpl.793:28|
+ :skolemid |24|
+ :pattern ( (|$IsValid'vec'u8''| v@@6))
+)))
+(assert (forall ((v@@7 T@Vec_2846) (e@@0 Int) ) (! (let ((i@@6 (|$IndexOfVec'u8'| v@@7 e@@0)))
+(ite  (not (exists ((i@@7 Int) ) (!  (and (and (|$IsValid'u64'| i@@7) (InRangeVec_2846 v@@7 i@@7)) (= (|Select__T@[Int]Int_| (|v#Vec_2846| v@@7) i@@7) e@@0))
+ :qid |outputbpl.800:13|
+ :skolemid |25|
+))) (= i@@6 (- 0 1))  (and (and (and (|$IsValid'u64'| i@@6) (InRangeVec_2846 v@@7 i@@6)) (= (|Select__T@[Int]Int_| (|v#Vec_2846| v@@7) i@@6) e@@0)) (forall ((j@@0 Int) ) (!  (=> (and (and (|$IsValid'u64'| j@@0) (>= j@@0 0)) (< j@@0 i@@6)) (not (= (|Select__T@[Int]Int_| (|v#Vec_2846| v@@7) j@@0) e@@0)))
+ :qid |outputbpl.808:17|
+ :skolemid |26|
+)))))
+ :qid |outputbpl.804:15|
+ :skolemid |27|
+ :pattern ( (|$IndexOfVec'u8'| v@@7 e@@0))
+)))
+(assert (forall ((v1@@1 T@Vec_2846) (v2@@1 T@Vec_2846) ) (! (= (|$IsEqual'vec'u8''| v1@@1 v2@@1) (|$IsEqual'vec'u8''| ($Hash_sha2 v1@@1) ($Hash_sha2 v2@@1)))
+ :qid |outputbpl.987:15|
+ :skolemid |28|
+ :pattern ( ($Hash_sha2 v1@@1) ($Hash_sha2 v2@@1))
+)))
+(assert (forall ((v1@@2 T@Vec_2846) (v2@@2 T@Vec_2846) ) (! (= (|$IsEqual'vec'u8''| v1@@2 v2@@2) (|$IsEqual'vec'u8''| ($Hash_sha3 v1@@2) ($Hash_sha3 v2@@2)))
+ :qid |outputbpl.1003:15|
+ :skolemid |29|
+ :pattern ( ($Hash_sha3 v1@@2) ($Hash_sha3 v2@@2))
+)))
+(assert (forall ((k1 T@Vec_2846) (k2 T@Vec_2846) ) (!  (=> (|$IsEqual'vec'u8''| k1 k2) (= ($Signature_$ed25519_validate_pubkey k1) ($Signature_$ed25519_validate_pubkey k2)))
+ :qid |outputbpl.1050:15|
+ :skolemid |30|
+ :pattern ( ($Signature_$ed25519_validate_pubkey k1) ($Signature_$ed25519_validate_pubkey k2))
+)))
+(assert (forall ((s1 T@Vec_2846) (s2 T@Vec_2846) (k1@@0 T@Vec_2846) (k2@@0 T@Vec_2846) (m1 T@Vec_2846) (m2 T@Vec_2846) ) (!  (=> (and (and (|$IsEqual'vec'u8''| s1 s2) (|$IsEqual'vec'u8''| k1@@0 k2@@0)) (|$IsEqual'vec'u8''| m1 m2)) (= ($Signature_$ed25519_verify s1 k1@@0 m1) ($Signature_$ed25519_verify s2 k2@@0 m2)))
+ :qid |outputbpl.1053:15|
+ :skolemid |31|
+ :pattern ( ($Signature_$ed25519_verify s1 k1@@0 m1) ($Signature_$ed25519_verify s2 k2@@0 m2))
+)))
+(assert (forall ((v@@8 T@Vec_2846) (i@@8 Int) ) (! (= (InRangeVec_2846 v@@8 i@@8)  (and (>= i@@8 0) (< i@@8 (|l#Vec_2846| v@@8))))
+ :qid |outputbpl.122:24|
+ :skolemid |3|
+ :pattern ( (InRangeVec_2846 v@@8 i@@8))
+)))
+(assert (forall ((v@@9 T@Vec_2846) (e@@1 Int) ) (! (let ((i@@9 (IndexOfVec_2846 v@@9 e@@1)))
+(ite  (not (exists ((i@@10 Int) ) (!  (and (InRangeVec_2846 v@@9 i@@10) (= (|Select__T@[Int]Int_| (|v#Vec_2846| v@@9) i@@10) e@@1))
+ :qid |outputbpl.109:13|
+ :skolemid |0|
+))) (= i@@9 (- 0 1))  (and (and (InRangeVec_2846 v@@9 i@@9) (= (|Select__T@[Int]Int_| (|v#Vec_2846| v@@9) i@@9) e@@1)) (forall ((j@@1 Int) ) (!  (=> (and (>= j@@1 0) (< j@@1 i@@9)) (not (= (|Select__T@[Int]Int_| (|v#Vec_2846| v@@9) j@@1) e@@1)))
+ :qid |outputbpl.117:17|
+ :skolemid |1|
+)))))
+ :qid |outputbpl.113:32|
+ :skolemid |2|
+ :pattern ( (IndexOfVec_2846 v@@9 e@@1))
+)))
+(assert (forall ((|l#0| Bool) (i@@11 Int) ) (! (= (|Select__T@[Int]Bool_| (|lambda#0| |l#0|) i@@11) |l#0|)
+ :qid |outputbpl.288:54|
+ :skolemid |36|
+ :pattern ( (|Select__T@[Int]Bool_| (|lambda#0| |l#0|) i@@11))
+)))
+(assert (forall ((|l#0@@0| Int) (|l#1| Int) (|l#2| Int) (|l#3| |T@[Int]Int|) (|l#4| |T@[Int]Int|) (|l#5| Int) (|l#6| Int) (i@@12 Int) ) (! (= (|Select__T@[Int]Int_| (|lambda#2| |l#0@@0| |l#1| |l#2| |l#3| |l#4| |l#5| |l#6|) i@@12) (ite  (and (>= i@@12 |l#0@@0|) (< i@@12 |l#1|)) (ite (< i@@12 |l#2|) (|Select__T@[Int]Int_| |l#3| i@@12) (|Select__T@[Int]Int_| |l#4| (- i@@12 |l#5|))) |l#6|))
+ :qid |outputbpl.73:19|
+ :skolemid |37|
+ :pattern ( (|Select__T@[Int]Int_| (|lambda#2| |l#0@@0| |l#1| |l#2| |l#3| |l#4| |l#5| |l#6|) i@@12))
+)))
+(assert (forall ((|l#0@@1| Int) (|l#1@@0| Int) (|l#2@@0| |T@[Int]Int|) (|l#3@@0| Int) (|l#4@@0| Int) (|l#5@@0| Int) (i@@13 Int) ) (! (= (|Select__T@[Int]Int_| (|lambda#3| |l#0@@1| |l#1@@0| |l#2@@0| |l#3@@0| |l#4@@0| |l#5@@0|) i@@13) (ite  (and (<= |l#0@@1| i@@13) (< i@@13 |l#1@@0|)) (|Select__T@[Int]Int_| |l#2@@0| (- (- |l#3@@0| i@@13) |l#4@@0|)) |l#5@@0|))
+ :qid |outputbpl.82:30|
+ :skolemid |38|
+ :pattern ( (|Select__T@[Int]Int_| (|lambda#3| |l#0@@1| |l#1@@0| |l#2@@0| |l#3@@0| |l#4@@0| |l#5@@0|) i@@13))
+)))
+(assert (forall ((|l#0@@2| Int) (|l#1@@1| Int) (|l#2@@1| Int) (|l#3@@1| |T@[Int]Int|) (|l#4@@1| |T@[Int]Int|) (|l#5@@1| Int) (|l#6@@0| Int) (j@@2 Int) ) (! (= (|Select__T@[Int]Int_| (|lambda#4| |l#0@@2| |l#1@@1| |l#2@@1| |l#3@@1| |l#4@@1| |l#5@@1| |l#6@@0|) j@@2) (ite  (and (>= j@@2 |l#0@@2|) (< j@@2 |l#1@@1|)) (ite (< j@@2 |l#2@@1|) (|Select__T@[Int]Int_| |l#3@@1| j@@2) (|Select__T@[Int]Int_| |l#4@@1| (+ j@@2 |l#5@@1|))) |l#6@@0|))
+ :qid |outputbpl.63:20|
+ :skolemid |39|
+ :pattern ( (|Select__T@[Int]Int_| (|lambda#4| |l#0@@2| |l#1@@1| |l#2@@1| |l#3@@1| |l#4@@1| |l#5@@1| |l#6@@0|) j@@2))
+)))
+(declare-fun ControlFlow (Int Int) Int)
+(declare-fun $t0@5 () T@Vec_2846)
+(declare-fun |inline$$Vector_push_back'u64'$2$m'@1| () T@$Mutation_8806)
+(declare-fun $t0@3 () T@Vec_2846)
+(declare-fun $t0@4 () T@Vec_2846)
+(declare-fun $t6@0 () T@$Mutation_8806)
+(declare-fun |Store__T@[Int]Int_| (|T@[Int]Int| Int Int) |T@[Int]Int|)
+(assert (forall ( ( ?x0 |T@[Int]Int|) ( ?x1 Int) ( ?x2 Int)) (! (= (|Select__T@[Int]Int_| (|Store__T@[Int]Int_| ?x0 ?x1 ?x2) ?x1)  ?x2) :weight 0)))
+(assert (forall ( ( ?x0 |T@[Int]Int|) ( ?x1 Int) ( ?y1 Int) ( ?x2 Int)) (! (=>  (not (= ?x1 ?y1)) (= (|Select__T@[Int]Int_| (|Store__T@[Int]Int_| ?x0 ?x1 ?x2) ?y1) (|Select__T@[Int]Int_| ?x0 ?y1))) :weight 0)))
+(declare-fun |inline$$Vector_push_back'u64'$1$m'@1| () T@$Mutation_8806)
+(declare-fun $t0@1 () T@Vec_2846)
+(declare-fun $t0@2 () T@Vec_2846)
+(declare-fun $t4@0 () T@$Mutation_8806)
+(declare-fun |inline$$Vector_push_back'u64'$0$m'@1| () T@$Mutation_8806)
+(declare-fun |inline$$Vector_empty'u64'$0$v@1| () T@Vec_2846)
+(declare-fun $t0@0 () T@Vec_2846)
+(declare-fun $t2@0 () T@$Mutation_8806)
+(declare-fun MapConstVec_3075 (Int) |T@[Int]Int|)
+(declare-fun DefaultVecElem_3075 () Int)
+(push 1)
+(set-info :boogie-vc-id $TestQuantInvariant_vector_of_proper_positives$verify)
+(assert (not
+ (=> (= (ControlFlow 0 0) 14811) (let ((anon14_correct  (=> (= $t0@5 $t0@5) (and (=> (= (ControlFlow 0 14024) (- 0 15219)) (not false)) (=> (not false) (and (=> (= (ControlFlow 0 14024) (- 0 15226)) (let (($range_0 $t0@5))
+(forall (($i_1 Int) ) (!  (=> (InRangeVec_2846 $range_0 $i_1) (let ((n (|Select__T@[Int]Int_| (|v#Vec_2846| $range_0) $i_1)))
+(> n 0)))
+ :qid |outputbpl.1223:37|
+ :skolemid |32|
+)))) (=> (let (($range_0 $t0@5))
+(forall (($i_1@@0 Int) ) (!  (=> (InRangeVec_2846 $range_0 $i_1@@0) (let ((n (|Select__T@[Int]Int_| (|v#Vec_2846| $range_0) $i_1@@0)))
+(> n 0)))
+ :qid |outputbpl.1223:37|
+ :skolemid |32|
+))) (and (=> (= (ControlFlow 0 14024) (- 0 15257)) (let (($range_0@@0 ($Range 0 (|l#Vec_2846| $t0@5))))
+(let (($range_1 ($Range 0 (|l#Vec_2846| $t0@5))))
+(forall (($i_2 Int) ($i_3 Int) ) (!  (=> ($InRange $range_0@@0 $i_2) (=> ($InRange $range_1 $i_3) (let ((i@@14 $i_2))
+(let ((j@@3 $i_3))
+ (=> (= (|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) i@@14) (|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) j@@3)) (= i@@14 j@@3))))))
+ :qid |outputbpl.1229:97|
+ :skolemid |33|
+))))) (=> (let (($range_0@@0 ($Range 0 (|l#Vec_2846| $t0@5))))
+(let (($range_1 ($Range 0 (|l#Vec_2846| $t0@5))))
+(forall (($i_2@@0 Int) ($i_3@@0 Int) ) (!  (=> ($InRange $range_0@@0 $i_2@@0) (=> ($InRange $range_1 $i_3@@0) (let ((i@@14 $i_2@@0))
+(let ((j@@3 $i_3@@0))
+ (=> (= (|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) i@@14) (|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) j@@3)) (= i@@14 j@@3))))))
+ :qid |outputbpl.1229:97|
+ :skolemid |33|
+)))) (and (=> (= (ControlFlow 0 14024) (- 0 15325)) (forall ((i@@15 Int) (j@@4 Int) ) (!  (=> (|$IsValid'u64'| i@@15) (=> (|$IsValid'u64'| j@@4) (=> (and (and (and (and (= (|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) i@@15) (|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) j@@4)) (>= i@@15 0)) (< i@@15 (|l#Vec_2846| $t0@5))) (>= j@@4 0)) (< j@@4 (|l#Vec_2846| $t0@5))) (= i@@15 j@@4))))
+ :qid |outputbpl.1236:15|
+ :skolemid |34|
+ :pattern ( (|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) i@@15) (|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) j@@4))
+))) (=> (forall ((i@@16 Int) (j@@5 Int) ) (!  (=> (|$IsValid'u64'| i@@16) (=> (|$IsValid'u64'| j@@5) (=> (and (and (and (and (= (|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) i@@16) (|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) j@@5)) (>= i@@16 0)) (< i@@16 (|l#Vec_2846| $t0@5))) (>= j@@5 0)) (< j@@5 (|l#Vec_2846| $t0@5))) (= i@@16 j@@5))))
+ :qid |outputbpl.1236:15|
+ :skolemid |34|
+ :pattern ( (|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) i@@16) (|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) j@@5))
+)) (=> (= (ControlFlow 0 14024) (- 0 15408)) (let (($range_0@@1 ($Range 0 (|l#Vec_2846| $t0@5))))
+(forall (($i_1@@1 Int) ) (!  (=> ($InRange $range_0@@1 $i_1@@1) (let ((i@@17 $i_1@@1))
+(let ((i@@18 (|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) i@@17)))
+(> i@@18 0))))
+ :qid |outputbpl.1241:56|
+ :skolemid |35|
+ :pattern ( (let ((i@@19 $i_1@@1))
+(|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) i@@19)) (let ((i@@20 $i_1@@1))
+(|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) i@@20)))
+ :pattern ( (let ((i@@21 $i_1@@1))
+(|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) i@@21)))
+)))))))))))))))
+(let ((anon22_Else_correct  (=> (not (= (|l#$Mutation_8806| |inline$$Vector_push_back'u64'$2$m'@1|) ($Local 0))) (=> (and (= $t0@5 $t0@3) (= (ControlFlow 0 13738) 14024)) anon14_correct))))
+(let ((anon22_Then_correct  (=> (and (and (= (|l#$Mutation_8806| |inline$$Vector_push_back'u64'$2$m'@1|) ($Local 0)) (= $t0@4 (|v#$Mutation_8806| |inline$$Vector_push_back'u64'$2$m'@1|))) (and (= $t0@5 $t0@4) (= (ControlFlow 0 14036) 14024))) anon14_correct)))
+(let ((anon21_Else_correct  (=> (not false) (and (=> (= (ControlFlow 0 13728) 14036) anon22_Then_correct) (=> (= (ControlFlow 0 13728) 13738) anon22_Else_correct)))))
+(let ((anon21_Then_correct true))
+(let ((|inline$$Vector_push_back'u64'$2$anon0_correct|  (=> (= |inline$$Vector_push_back'u64'$2$m'@1| ($Mutation_8806 (|l#$Mutation_8806| $t6@0) (|p#$Mutation_8806| $t6@0) (let ((l (|l#Vec_2846| (|v#$Mutation_8806| $t6@0))))
+(Vec_2846 (|Store__T@[Int]Int_| (|v#Vec_2846| (|v#$Mutation_8806| $t6@0)) l 3) (+ l 1))))) (and (=> (= (ControlFlow 0 13714) 14050) anon21_Then_correct) (=> (= (ControlFlow 0 13714) 13728) anon21_Else_correct)))))
+(let ((anon10_correct  (=> (= $t6@0 ($Mutation_8806 ($Local 0) $EmptyPath $t0@3)) (=> (and (|$IsValid'u64'| 3) (= (ControlFlow 0 13720) 13714)) |inline$$Vector_push_back'u64'$2$anon0_correct|))))
+(let ((anon20_Else_correct  (=> (not (= (|l#$Mutation_8806| |inline$$Vector_push_back'u64'$1$m'@1|) ($Local 0))) (=> (and (= $t0@3 $t0@1) (= (ControlFlow 0 13643) 13720)) anon10_correct))))
+(let ((anon20_Then_correct  (=> (and (and (= (|l#$Mutation_8806| |inline$$Vector_push_back'u64'$1$m'@1|) ($Local 0)) (= $t0@2 (|v#$Mutation_8806| |inline$$Vector_push_back'u64'$1$m'@1|))) (and (= $t0@3 $t0@2) (= (ControlFlow 0 14072) 13720))) anon10_correct)))
+(let ((anon19_Else_correct  (=> (not false) (and (=> (= (ControlFlow 0 13633) 14072) anon20_Then_correct) (=> (= (ControlFlow 0 13633) 13643) anon20_Else_correct)))))
+(let ((anon19_Then_correct true))
+(let ((|inline$$Vector_push_back'u64'$1$anon0_correct|  (=> (= |inline$$Vector_push_back'u64'$1$m'@1| ($Mutation_8806 (|l#$Mutation_8806| $t4@0) (|p#$Mutation_8806| $t4@0) (let ((l@@0 (|l#Vec_2846| (|v#$Mutation_8806| $t4@0))))
+(Vec_2846 (|Store__T@[Int]Int_| (|v#Vec_2846| (|v#$Mutation_8806| $t4@0)) l@@0 2) (+ l@@0 1))))) (and (=> (= (ControlFlow 0 13619) 14086) anon19_Then_correct) (=> (= (ControlFlow 0 13619) 13633) anon19_Else_correct)))))
+(let ((anon6_correct  (=> (= $t4@0 ($Mutation_8806 ($Local 0) $EmptyPath $t0@1)) (=> (and (|$IsValid'u64'| 2) (= (ControlFlow 0 13625) 13619)) |inline$$Vector_push_back'u64'$1$anon0_correct|))))
+(let ((anon18_Else_correct  (=> (not (= (|l#$Mutation_8806| |inline$$Vector_push_back'u64'$0$m'@1|) ($Local 0))) (=> (and (= $t0@1 |inline$$Vector_empty'u64'$0$v@1|) (= (ControlFlow 0 13548) 13625)) anon6_correct))))
+(let ((anon18_Then_correct  (=> (and (and (= (|l#$Mutation_8806| |inline$$Vector_push_back'u64'$0$m'@1|) ($Local 0)) (= $t0@0 (|v#$Mutation_8806| |inline$$Vector_push_back'u64'$0$m'@1|))) (and (= $t0@1 $t0@0) (= (ControlFlow 0 14098) 13625))) anon6_correct)))
+(let ((anon17_Else_correct  (=> (not false) (and (=> (= (ControlFlow 0 13538) 14098) anon18_Then_correct) (=> (= (ControlFlow 0 13538) 13548) anon18_Else_correct)))))
+(let ((anon17_Then_correct true))
+(let ((|inline$$Vector_push_back'u64'$0$anon0_correct|  (=> (= |inline$$Vector_push_back'u64'$0$m'@1| ($Mutation_8806 (|l#$Mutation_8806| $t2@0) (|p#$Mutation_8806| $t2@0) (let ((l@@1 (|l#Vec_2846| (|v#$Mutation_8806| $t2@0))))
+(Vec_2846 (|Store__T@[Int]Int_| (|v#Vec_2846| (|v#$Mutation_8806| $t2@0)) l@@1 1) (+ l@@1 1))))) (and (=> (= (ControlFlow 0 13524) 14112) anon17_Then_correct) (=> (= (ControlFlow 0 13524) 13538) anon17_Else_correct)))))
+(let ((anon16_Else_correct  (=> (not false) (=> (and (and (= |inline$$Vector_empty'u64'$0$v@1| |inline$$Vector_empty'u64'$0$v@1|) (= $t2@0 ($Mutation_8806 ($Local 0) $EmptyPath |inline$$Vector_empty'u64'$0$v@1|))) (and (|$IsValid'u64'| 1) (= (ControlFlow 0 13530) 13524))) |inline$$Vector_push_back'u64'$0$anon0_correct|))))
+(let ((anon16_Then_correct true))
+(let ((|inline$$Vector_empty'u64'$0$anon0_correct|  (=> (= |inline$$Vector_empty'u64'$0$v@1| (Vec_2846 (MapConstVec_3075 DefaultVecElem_3075) 0)) (and (=> (= (ControlFlow 0 13435) 14126) anon16_Then_correct) (=> (= (ControlFlow 0 13435) 13530) anon16_Else_correct)))))
+(let ((anon0$1_correct  (=> (= (ControlFlow 0 13441) 13435) |inline$$Vector_empty'u64'$0$anon0_correct|)))
+(let ((anon0_correct  (=> (= (ControlFlow 0 14811) 13441) anon0$1_correct)))
+anon0_correct))))))))))))))))))))))))
+))
+(check-sat)