From 0b171fc7751344f94bbe7a868156dd918bec950d Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Tue, 11 Aug 2026 20:02:00 -0500 Subject: [PATCH] Update the multiple_solvers test output cvc5 changed the error message reported when a term outside the declared logic reaches preprocessing: "got a theory atom for that theory" is now "got a preprocessing-time term for that theory", and the term printed is the offending subterm `(* 2 y)` rather than the atom `(= x (* 2 y))`. Refresh the expected output accordingly. Co-Authored-By: Claude Opus 5 (1M context) --- test/pgm_outputs/multiple_solvers.py.out | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/test/pgm_outputs/multiple_solvers.py.out b/test/pgm_outputs/multiple_solvers.py.out index fbc8671..9261ef4 100644 --- a/test/pgm_outputs/multiple_solvers.py.out +++ b/test/pgm_outputs/multiple_solvers.py.out @@ -1,9 +1,9 @@ [x = 0, y = 0] sat 0 -The logic was specified as QF_BV, which doesn't include THEORY_ARITH, but got a theory atom for that theory. -The atom: -(= x (* 2 y)) +The logic was specified as QF_BV, which doesn't include THEORY_ARITH, but got a preprocessing-time term for that theory. +The term: +(* 2 y) Can't solve integer problems with QF_BV solver got an exception, which is good unsat