From 8de2503f9f2cc2d0c16f38209716140dad95a5d7 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 29 Jan 2024 16:51:10 +0100 Subject: [PATCH] bugfix? --- src/sat/smt/polysat/monomials.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/smt/polysat/monomials.cpp b/src/sat/smt/polysat/monomials.cpp index ee0bec436..e292eb3fa 100644 --- a/src/sat/smt/polysat/monomials.cpp +++ b/src/sat/smt/polysat/monomials.cpp @@ -180,7 +180,7 @@ namespace polysat { pdd qs = c.value(rational(1), mon.num_bits()); for (unsigned k = mon.size(); k-- > 0; ) if (k != j) - qs *= mon.arg_vals[k]; + qs *= mon.args[k]; c.add_axiom("p * q = p => q = 1 or p = 0", { ~C.eq(mon.var, p), C.eq(qs, 1), C.eq(p) }, true); return true; }