From cbcb5ad92d9ee630561c8a36dfeac7cd8ef7b9d7 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 7 Feb 2024 15:21:47 +0100 Subject: [PATCH] euf::theory_var is int --- src/sat/smt/polysat/types.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/smt/polysat/types.h b/src/sat/smt/polysat/types.h index af8718523..39d30468a 100644 --- a/src/sat/smt/polysat/types.h +++ b/src/sat/smt/polysat/types.h @@ -21,7 +21,7 @@ namespace polysat { using pdd = dd::pdd; using pvar = unsigned; - using theory_var = unsigned; + using theory_var = int; struct constraint_id { unsigned id = UINT_MAX; bool is_null() const { return id == UINT_MAX; }