From d125d87aed403edaf2e971f4038e573eaba708c6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 6 Dec 2022 15:51:38 -0800
Subject: [PATCH] typo

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/core/solve_eqs_tactic.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/tactic/core/solve_eqs_tactic.h b/src/tactic/core/solve_eqs_tactic.h
index 604bcf426..fec46bf04 100644
--- a/src/tactic/core/solve_eqs_tactic.h
+++ b/src/tactic/core/solve_eqs_tactic.h
@@ -35,7 +35,7 @@ everywhere by `f(x + y)`. It depends on a set of theory specific equality solver
 * Arithmetic equations
   * It solves `x mod k = s` to `x = k * m' + s`, where m'` is a fresh constant. 
   * It finds variables with unit coefficients in integer linear equations.
-  * It solves for `x * Y = Z$ under the side-condition `Y != 0` as `x = Z/Y`.
+  * It solves for `x * Y = Z` under the side-condition `Y != 0` as `x = Z/Y`.
  
 It also allows solving for uninterpreted constants that only appear in a single disjuction. For example, 
 `(or (= x (+ 5 y)) (= y (+ u z)))` allows solving for `x`.