From 37bf5fefca0bfc056e0f071303046c32a7cab3ec Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 12 Mar 2024 13:47:23 +0100
Subject: [PATCH] fix extract axiom

---
 src/sat/smt/polysat_internalize.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp
index 535cae8f9..7b65d3d01 100644
--- a/src/sat/smt/polysat_internalize.cpp
+++ b/src/sat/smt/polysat_internalize.cpp
@@ -1,4 +1,4 @@
-/*++
+/*++
 Copyright (c) 2022 Microsoft Corporation
 
 Module Name:
@@ -741,7 +741,7 @@ namespace polysat {
         auto gelo = mk_literal(bv.mk_ule(bv.mk_numeral(rational::power_of_two(lo), sz_x), x));
         auto name = "extract";
         add_axiom(name, { eq0, gelo });
-        if (hi + 1 == sz_e)
+        if (hi + 1 == sz_x)
             add_axiom(name, { ~eq0, ~gelo });
     }