From c85c0489478dfc8943f9a3a19c8d8982fa1ff008 Mon Sep 17 00:00:00 2001 From: Paul Wagner Date: Mon, 15 Jul 2024 15:08:18 +0200 Subject: [PATCH] Fix missing variables from objective function in NRA --- .../theory/solver/NonLinearRealArithmeticSolver.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/main/java/me/paultristanwagner/satchecking/theory/solver/NonLinearRealArithmeticSolver.java b/src/main/java/me/paultristanwagner/satchecking/theory/solver/NonLinearRealArithmeticSolver.java index 7550d00..76d897c 100644 --- a/src/main/java/me/paultristanwagner/satchecking/theory/solver/NonLinearRealArithmeticSolver.java +++ b/src/main/java/me/paultristanwagner/satchecking/theory/solver/NonLinearRealArithmeticSolver.java @@ -60,6 +60,8 @@ public TheoryResult solve() { List variableOrdering = null; String freshVariableName = null; if (objective != null) { + variablesSet.addAll(objective.getObjective().variables); + freshVariableName = freshVariableName(variablesSet); MultivariatePolynomial freshVariable = variable(freshVariableName); MultivariatePolynomialConstraint helper = MultivariatePolynomialConstraint.equals(freshVariable, objective.getObjective());