From 6e53621146accfea773595e1db66d98c5b7b978e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 5 Jul 2022 13:17:04 -0700
Subject: [PATCH] #6112

add q->get_qid() to comparison of quantifiers
---
 src/ast/ast.cpp | 42 +++++++++++++++++++++++-------------------
 1 file changed, 23 insertions(+), 19 deletions(-)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 5c48f31d0..468ad8c81 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -471,26 +471,30 @@ bool compare_nodes(ast const * n1, ast const * n2) {
         return
             to_var(n1)->get_idx()  == to_var(n2)->get_idx() &&
             to_var(n1)->get_sort() == to_var(n2)->get_sort();
-    case AST_QUANTIFIER:
+    case AST_QUANTIFIER: {
+        quantifier const* q1 = to_quantifier(n1);
+        quantifier const* q2 = to_quantifier(n2);
         return
-            to_quantifier(n1)->get_kind()            == to_quantifier(n2)->get_kind() &&
-            to_quantifier(n1)->get_num_decls()       == to_quantifier(n2)->get_num_decls() &&
-            compare_arrays(to_quantifier(n1)->get_decl_sorts(),
-                           to_quantifier(n2)->get_decl_sorts(),
-                           to_quantifier(n1)->get_num_decls()) &&
-            compare_arrays(to_quantifier(n1)->get_decl_names(),
-                           to_quantifier(n2)->get_decl_names(),
-                           to_quantifier(n1)->get_num_decls()) &&
-            to_quantifier(n1)->get_expr()            == to_quantifier(n2)->get_expr() &&
-            to_quantifier(n1)->get_weight()          == to_quantifier(n2)->get_weight() &&
-            to_quantifier(n1)->get_num_patterns() == to_quantifier(n2)->get_num_patterns() &&
-            compare_arrays(to_quantifier(n1)->get_patterns(),
-                           to_quantifier(n2)->get_patterns(),
-                           to_quantifier(n1)->get_num_patterns()) &&
-            to_quantifier(n1)->get_num_no_patterns() == to_quantifier(n2)->get_num_no_patterns() &&
-            compare_arrays(to_quantifier(n1)->get_no_patterns(),
-                           to_quantifier(n2)->get_no_patterns(),
-                           to_quantifier(n1)->get_num_no_patterns());
+            q1->get_kind()         == q2->get_kind() &&
+            q1->get_num_decls()    == q2->get_num_decls() &&
+            compare_arrays(q1->get_decl_sorts(),
+                           q2->get_decl_sorts(),
+                           q1->get_num_decls()) &&
+            compare_arrays(q1->get_decl_names(),
+                           q2->get_decl_names(),
+                           q1->get_num_decls()) &&
+            q1->get_expr()         == q2->get_expr() &&
+            q1->get_weight()       == q2->get_weight() &&
+            q1->get_num_patterns() == q2->get_num_patterns() &&
+            q1->get_qid() == q2->get_qid() && 
+            compare_arrays(q1->get_patterns(),
+                           q2->get_patterns(),
+                           q1->get_num_patterns()) &&
+            q1->get_num_no_patterns() == q2->get_num_no_patterns() &&
+            compare_arrays(q1->get_no_patterns(),
+                           q2->get_no_patterns(),
+                           q1->get_num_no_patterns());
+    }
     default:
         UNREACHABLE();
     }