Skip to content

Commit

Permalink
typo
Browse files Browse the repository at this point in the history
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
  • Loading branch information
NikolajBjorner committed Dec 6, 2022
1 parent 1e06c74 commit d125d87
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/tactic/core/solve_eqs_tactic.h
Original file line number Diff line number Diff line change
Expand Up @@ -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`.
Expand Down

0 comments on commit d125d87

Please sign in to comment.