projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: f28ed39)
Discard duplicate terms in patterns (#6501)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 6 May 2021 21:57:37 +0000 (16:57 -0500)
committerGitHub <noreply@github.com>
Thu, 6 May 2021 21:57:37 +0000 (18:57 -0300)
Fixes #6495.

src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp patch | blob | history
test/regress/CMakeLists.txt patch | blob | history
test/regress/regress2/issue6495-dup-pat-term.smt2 [new file with mode: 0644] patch | blob

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 193ba250edbd1ff45271c0757ecf4bfc4388b809..a937edf444a7a04c357b1a1ed8e548de259169a8 100644 (file)
--- 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 3f1ff1307b8787c4e6601e4670f2dd0c1d7f3749..a64a1eb1e5c1e83c51c116feff9ae11e4119b23a 100644 (file)
--- 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 (file)
index 0000000..3c8d0df
--- /dev/null
+++ b/test/regress/regress2/issue6495-dup-pat-term.smt2
@@ -0,0 +1,298 @@
+; COMMAND-LINE: -i -q\r
+; EXPECT: unsat\r
+(set-logic ALL_SUPPORTED)\r
+(set-info :status unsat)\r
+(declare-sort |T@[Int]Int| 0)\r
+(declare-datatypes ((T@Vec_2846 0)) (((Vec_2846 (|v#Vec_2846| |T@[Int]Int|) (|l#Vec_2846| Int) ) ) ))\r
+(declare-datatypes ((T@$Location 0)) ((($Global (|a#$Global| Int) ) ($Local (|i#$Local| Int) ) ($Param (|i#$Param| Int) ) ) ))\r
+(declare-datatypes ((T@$Path 0)) ((($Path (|p#$Path| |T@[Int]Int|) (|size#$Path| Int) ) ) ))\r
+(declare-datatypes ((T@$Mutation_3470 0)) ((($Mutation_3470 (|l#$Mutation_3470| T@$Location) (|p#$Mutation_3470| T@$Path) (|v#$Mutation_3470| Int) ) ) ))\r
+(declare-datatypes ((T@$Mutation_8806 0)) ((($Mutation_8806 (|l#$Mutation_8806| T@$Location) (|p#$Mutation_8806| T@$Path) (|v#$Mutation_8806| T@Vec_2846) ) ) ))\r
+(declare-datatypes ((T@$Range 0)) ((($Range (|lb#$Range| Int) (|ub#$Range| Int) ) ) ))\r
+(declare-fun $MAX_U8 () Int)\r
+(declare-fun $MAX_U64 () Int)\r
+(declare-fun $MAX_U128 () Int)\r
+(declare-fun |$IsValid'u8'| (Int) Bool)\r
+(declare-fun |$IsValid'u64'| (Int) Bool)\r
+(declare-fun |$IsValid'u128'| (Int) Bool)\r
+(declare-fun |$IsValid'num'| (Int) Bool)\r
+(declare-fun |$IsValid'address'| (Int) Bool)\r
+(declare-fun $InRange (T@$Range Int) Bool)\r
+(declare-fun $EmptyPath () T@$Path)\r
+(declare-sort |T@[Int]Bool| 0)\r
+(declare-fun $ConstMemoryDomain (Bool) |T@[Int]Bool|)\r
+(declare-fun |lambda#0| (Bool) |T@[Int]Bool|)\r
+(declare-fun $EXEC_FAILURE_CODE () Int)\r
+(declare-fun $shl (Int Int) Int)\r
+(declare-fun $shr (Int Int) Int)\r
+(declare-fun |$IsEqual'vec'u64''| (T@Vec_2846 T@Vec_2846) Bool)\r
+(declare-fun InRangeVec_2846 (T@Vec_2846 Int) Bool)\r
+(declare-fun |Select__T@[Int]Int_| (|T@[Int]Int| Int) Int)\r
+(declare-fun |$IsValid'vec'u64''| (T@Vec_2846) Bool)\r
+(declare-fun |$IndexOfVec'u64'| (T@Vec_2846 Int) Int)\r
+(declare-fun |$IsEqual'vec'u8''| (T@Vec_2846 T@Vec_2846) Bool)\r
+(declare-fun |$IsValid'vec'u8''| (T@Vec_2846) Bool)\r
+(declare-fun |$IndexOfVec'u8'| (T@Vec_2846 Int) Int)\r
+(declare-fun $Hash_sha2 (T@Vec_2846) T@Vec_2846)\r
+(declare-fun $Hash_sha3 (T@Vec_2846) T@Vec_2846)\r
+(declare-fun $Signature_$ed25519_validate_pubkey (T@Vec_2846) Bool)\r
+(declare-fun $Signature_$ed25519_verify (T@Vec_2846 T@Vec_2846 T@Vec_2846) Bool)\r
+(declare-fun IndexOfVec_2846 (T@Vec_2846 Int) Int)\r
+(declare-fun |Select__T@[Int]Bool_| (|T@[Int]Bool| Int) Bool)\r
+(declare-fun |lambda#2| (Int Int Int |T@[Int]Int| |T@[Int]Int| Int Int) |T@[Int]Int|)\r
+(declare-fun |lambda#3| (Int Int |T@[Int]Int| Int Int Int) |T@[Int]Int|)\r
+(declare-fun |lambda#4| (Int Int Int |T@[Int]Int| |T@[Int]Int| Int Int) |T@[Int]Int|)\r
+(assert (= $MAX_U8 255))\r
+(assert (= $MAX_U64 18446744073709551615))\r
+(assert (= $MAX_U128 340282366920938463463374607431768211455))\r
+(assert (forall ((v Int) ) (! (= (|$IsValid'u8'| v)  (and (>= v 0) (<= v $MAX_U8)))\r
+ :qid |outputbpl.190:23|\r
+ :skolemid |6|\r
+ :pattern ( (|$IsValid'u8'| v))\r
+)))\r
+(assert (forall ((v@@0 Int) ) (! (= (|$IsValid'u64'| v@@0)  (and (>= v@@0 0) (<= v@@0 $MAX_U64)))\r
+ :qid |outputbpl.194:24|\r
+ :skolemid |7|\r
+ :pattern ( (|$IsValid'u64'| v@@0))\r
+)))\r
+(assert (forall ((v@@1 Int) ) (! (= (|$IsValid'u128'| v@@1)  (and (>= v@@1 0) (<= v@@1 $MAX_U128)))\r
+ :qid |outputbpl.198:25|\r
+ :skolemid |8|\r
+ :pattern ( (|$IsValid'u128'| v@@1))\r
+)))\r
+(assert (forall ((v@@2 Int) ) (! (= (|$IsValid'num'| v@@2) true)\r
+ :qid |outputbpl.202:24|\r
+ :skolemid |9|\r
+ :pattern ( (|$IsValid'num'| v@@2))\r
+)))\r
+(assert (forall ((v@@3 Int) ) (! (= (|$IsValid'address'| v@@3) (>= v@@3 0))\r
+ :qid |outputbpl.206:28|\r
+ :skolemid |10|\r
+ :pattern ( (|$IsValid'address'| v@@3))\r
+)))\r
+(assert (forall ((r T@$Range) (i Int) ) (! (= ($InRange r i)  (and (<= (|lb#$Range| r) i) (< i (|ub#$Range| r))))\r
+ :qid |outputbpl.216:19|\r
+ :skolemid |11|\r
+ :pattern ( ($InRange r i))\r
+)))\r
+(assert (= (|size#$Path| $EmptyPath) 0))\r
+(assert (= ($ConstMemoryDomain false) (|lambda#0| false)))\r
+(assert (= ($ConstMemoryDomain true) (|lambda#0| true)))\r
+(assert (= $EXEC_FAILURE_CODE (- 0 1)))\r
+(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))))))\r
+ :qid |outputbpl.469:15|\r
+ :skolemid |12|\r
+ :pattern ( ($shl src1 p))\r
+)))\r
+(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))))))\r
+ :qid |outputbpl.478:15|\r
+ :skolemid |13|\r
+ :pattern ( ($shr src1@@0 p@@0))\r
+)))\r
+(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)))\r
+ :qid |outputbpl.602:13|\r
+ :skolemid |14|\r
+))))\r
+ :qid |outputbpl.600:29|\r
+ :skolemid |15|\r
+ :pattern ( (|$IsEqual'vec'u64''| v1 v2))\r
+)))\r
+(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)))\r
+ :qid |outputbpl.608:13|\r
+ :skolemid |16|\r
+))))\r
+ :qid |outputbpl.606:29|\r
+ :skolemid |17|\r
+ :pattern ( (|$IsValid'vec'u64''| v@@4))\r
+)))\r
+(assert (forall ((v@@5 T@Vec_2846) (e Int) ) (! (let ((i@@2 (|$IndexOfVec'u64'| v@@5 e)))\r
+(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))\r
+ :qid |outputbpl.613:13|\r
+ :skolemid |18|\r
+))) (= 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)))\r
+ :qid |outputbpl.621:17|\r
+ :skolemid |19|\r
+)))))\r
+ :qid |outputbpl.617:15|\r
+ :skolemid |20|\r
+ :pattern ( (|$IndexOfVec'u64'| v@@5 e))\r
+)))\r
+(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)))\r
+ :qid |outputbpl.789:13|\r
+ :skolemid |21|\r
+))))\r
+ :qid |outputbpl.787:28|\r
+ :skolemid |22|\r
+ :pattern ( (|$IsEqual'vec'u8''| v1@@0 v2@@0))\r
+)))\r
+(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)))\r
+ :qid |outputbpl.795:13|\r
+ :skolemid |23|\r
+))))\r
+ :qid |outputbpl.793:28|\r
+ :skolemid |24|\r
+ :pattern ( (|$IsValid'vec'u8''| v@@6))\r
+)))\r
+(assert (forall ((v@@7 T@Vec_2846) (e@@0 Int) ) (! (let ((i@@6 (|$IndexOfVec'u8'| v@@7 e@@0)))\r
+(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))\r
+ :qid |outputbpl.800:13|\r
+ :skolemid |25|\r
+))) (= 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)))\r
+ :qid |outputbpl.808:17|\r
+ :skolemid |26|\r
+)))))\r
+ :qid |outputbpl.804:15|\r
+ :skolemid |27|\r
+ :pattern ( (|$IndexOfVec'u8'| v@@7 e@@0))\r
+)))\r
+(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)))\r
+ :qid |outputbpl.987:15|\r
+ :skolemid |28|\r
+ :pattern ( ($Hash_sha2 v1@@1) ($Hash_sha2 v2@@1))\r
+)))\r
+(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)))\r
+ :qid |outputbpl.1003:15|\r
+ :skolemid |29|\r
+ :pattern ( ($Hash_sha3 v1@@2) ($Hash_sha3 v2@@2))\r
+)))\r
+(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)))\r
+ :qid |outputbpl.1050:15|\r
+ :skolemid |30|\r
+ :pattern ( ($Signature_$ed25519_validate_pubkey k1) ($Signature_$ed25519_validate_pubkey k2))\r
+)))\r
+(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)))\r
+ :qid |outputbpl.1053:15|\r
+ :skolemid |31|\r
+ :pattern ( ($Signature_$ed25519_verify s1 k1@@0 m1) ($Signature_$ed25519_verify s2 k2@@0 m2))\r
+)))\r
+(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))))\r
+ :qid |outputbpl.122:24|\r
+ :skolemid |3|\r
+ :pattern ( (InRangeVec_2846 v@@8 i@@8))\r
+)))\r
+(assert (forall ((v@@9 T@Vec_2846) (e@@1 Int) ) (! (let ((i@@9 (IndexOfVec_2846 v@@9 e@@1)))\r
+(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))\r
+ :qid |outputbpl.109:13|\r
+ :skolemid |0|\r
+))) (= 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)))\r
+ :qid |outputbpl.117:17|\r
+ :skolemid |1|\r
+)))))\r
+ :qid |outputbpl.113:32|\r
+ :skolemid |2|\r
+ :pattern ( (IndexOfVec_2846 v@@9 e@@1))\r
+)))\r
+(assert (forall ((|l#0| Bool) (i@@11 Int) ) (! (= (|Select__T@[Int]Bool_| (|lambda#0| |l#0|) i@@11) |l#0|)\r
+ :qid |outputbpl.288:54|\r
+ :skolemid |36|\r
+ :pattern ( (|Select__T@[Int]Bool_| (|lambda#0| |l#0|) i@@11))\r
+)))\r
+(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|))\r
+ :qid |outputbpl.73:19|\r
+ :skolemid |37|\r
+ :pattern ( (|Select__T@[Int]Int_| (|lambda#2| |l#0@@0| |l#1| |l#2| |l#3| |l#4| |l#5| |l#6|) i@@12))\r
+)))\r
+(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|))\r
+ :qid |outputbpl.82:30|\r
+ :skolemid |38|\r
+ :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))\r
+)))\r
+(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|))\r
+ :qid |outputbpl.63:20|\r
+ :skolemid |39|\r
+ :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))\r
+)))\r
+(declare-fun ControlFlow (Int Int) Int)\r
+(declare-fun $t0@5 () T@Vec_2846)\r
+(declare-fun |inline$$Vector_push_back'u64'$2$m'@1| () T@$Mutation_8806)\r
+(declare-fun $t0@3 () T@Vec_2846)\r
+(declare-fun $t0@4 () T@Vec_2846)\r
+(declare-fun $t6@0 () T@$Mutation_8806)\r
+(declare-fun |Store__T@[Int]Int_| (|T@[Int]Int| Int Int) |T@[Int]Int|)\r
+(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)))\r
+(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)))\r
+(declare-fun |inline$$Vector_push_back'u64'$1$m'@1| () T@$Mutation_8806)\r
+(declare-fun $t0@1 () T@Vec_2846)\r
+(declare-fun $t0@2 () T@Vec_2846)\r
+(declare-fun $t4@0 () T@$Mutation_8806)\r
+(declare-fun |inline$$Vector_push_back'u64'$0$m'@1| () T@$Mutation_8806)\r
+(declare-fun |inline$$Vector_empty'u64'$0$v@1| () T@Vec_2846)\r
+(declare-fun $t0@0 () T@Vec_2846)\r
+(declare-fun $t2@0 () T@$Mutation_8806)\r
+(declare-fun MapConstVec_3075 (Int) |T@[Int]Int|)\r
+(declare-fun DefaultVecElem_3075 () Int)\r
+(push 1)\r
+(set-info :boogie-vc-id $TestQuantInvariant_vector_of_proper_positives$verify)\r
+(assert (not\r
+ (=> (= (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))\r
+(forall (($i_1 Int) ) (!  (=> (InRangeVec_2846 $range_0 $i_1) (let ((n (|Select__T@[Int]Int_| (|v#Vec_2846| $range_0) $i_1)))\r
+(> n 0)))\r
+ :qid |outputbpl.1223:37|\r
+ :skolemid |32|\r
+)))) (=> (let (($range_0 $t0@5))\r
+(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)))\r
+(> n 0)))\r
+ :qid |outputbpl.1223:37|\r
+ :skolemid |32|\r
+))) (and (=> (= (ControlFlow 0 14024) (- 0 15257)) (let (($range_0@@0 ($Range 0 (|l#Vec_2846| $t0@5))))\r
+(let (($range_1 ($Range 0 (|l#Vec_2846| $t0@5))))\r
+(forall (($i_2 Int) ($i_3 Int) ) (!  (=> ($InRange $range_0@@0 $i_2) (=> ($InRange $range_1 $i_3) (let ((i@@14 $i_2))\r
+(let ((j@@3 $i_3))\r
+ (=> (= (|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))))))\r
+ :qid |outputbpl.1229:97|\r
+ :skolemid |33|\r
+))))) (=> (let (($range_0@@0 ($Range 0 (|l#Vec_2846| $t0@5))))\r
+(let (($range_1 ($Range 0 (|l#Vec_2846| $t0@5))))\r
+(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))\r
+(let ((j@@3 $i_3@@0))\r
+ (=> (= (|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))))))\r
+ :qid |outputbpl.1229:97|\r
+ :skolemid |33|\r
+)))) (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))))\r
+ :qid |outputbpl.1236:15|\r
+ :skolemid |34|\r
+ :pattern ( (|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) i@@15) (|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) j@@4))\r
+))) (=> (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))))\r
+ :qid |outputbpl.1236:15|\r
+ :skolemid |34|\r
+ :pattern ( (|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) i@@16) (|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) j@@5))\r
+)) (=> (= (ControlFlow 0 14024) (- 0 15408)) (let (($range_0@@1 ($Range 0 (|l#Vec_2846| $t0@5))))\r
+(forall (($i_1@@1 Int) ) (!  (=> ($InRange $range_0@@1 $i_1@@1) (let ((i@@17 $i_1@@1))\r
+(let ((i@@18 (|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) i@@17)))\r
+(> i@@18 0))))\r
+ :qid |outputbpl.1241:56|\r
+ :skolemid |35|\r
+ :pattern ( (let ((i@@19 $i_1@@1))\r
+(|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) i@@19)) (let ((i@@20 $i_1@@1))\r
+(|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) i@@20)))\r
+ :pattern ( (let ((i@@21 $i_1@@1))\r
+(|Select__T@[Int]Int_| (|v#Vec_2846| $t0@5) i@@21)))\r
+)))))))))))))))\r
+(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))))\r
+(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)))\r
+(let ((anon21_Else_correct  (=> (not false) (and (=> (= (ControlFlow 0 13728) 14036) anon22_Then_correct) (=> (= (ControlFlow 0 13728) 13738) anon22_Else_correct)))))\r
+(let ((anon21_Then_correct true))\r
+(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))))\r
+(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)))))\r
+(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|))))\r
+(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))))\r
+(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)))\r
+(let ((anon19_Else_correct  (=> (not false) (and (=> (= (ControlFlow 0 13633) 14072) anon20_Then_correct) (=> (= (ControlFlow 0 13633) 13643) anon20_Else_correct)))))\r
+(let ((anon19_Then_correct true))\r
+(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))))\r
+(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)))))\r
+(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|))))\r
+(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))))\r
+(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)))\r
+(let ((anon17_Else_correct  (=> (not false) (and (=> (= (ControlFlow 0 13538) 14098) anon18_Then_correct) (=> (= (ControlFlow 0 13538) 13548) anon18_Else_correct)))))\r
+(let ((anon17_Then_correct true))\r
+(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))))\r
+(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)))))\r
+(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|))))\r
+(let ((anon16_Then_correct true))\r
+(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)))))\r
+(let ((anon0$1_correct  (=> (= (ControlFlow 0 13441) 13435) |inline$$Vector_empty'u64'$0$anon0_correct|)))\r
+(let ((anon0_correct  (=> (= (ControlFlow 0 14811) 13441) anon0$1_correct)))\r
+anon0_correct))))))))))))))))))))))))\r
+))\r
+(check-sat)\r