From 839b7101aef34dce0a33147642f93e0994222e2b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 22 Jan 2024 15:48:03 -0800
Subject: [PATCH] add ability to multiply term

---
 src/math/lp/lar_term.h | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/math/lp/lar_term.h b/src/math/lp/lar_term.h
index 5ce1ff2fc..a96d3ad5a 100644
--- a/src/math/lp/lar_term.h
+++ b/src/math/lp/lar_term.h
@@ -138,6 +138,12 @@ public:
         }
         return ret;
     }
+
+    lar_term& operator*=(mpq const& k) {
+        for (auto & t : m_coeffs)
+            t.m_value *= k;
+        return *this;
+    }
    
     void clear() {
         m_coeffs.reset();