From ea1f107a92f22961a50fbc51d93780f89cbd66e0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 27 Mar 2020 17:45:30 -0500 Subject: [PATCH] Fix expected output on arith regression (#4162) A benchmark went unknown -> sat, likely due to the arith-brab commit, thus leading to a failure on regress1.This updates the status on this benchmark (also adds --nl-ext-tplanes to it). --- test/regress/regress1/arith/bug547.1.smt2 | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/regress/regress1/arith/bug547.1.smt2 b/test/regress/regress1/arith/bug547.1.smt2 index 4b7cf9780..38d1dfcb1 100644 --- a/test/regress/regress1/arith/bug547.1.smt2 +++ b/test/regress/regress1/arith/bug547.1.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: --rewrite-divk -; EXPECT: unknown +; COMMAND-LINE: --rewrite-divk --nl-ext-tplanes +; EXPECT: sat (set-logic QF_NIA) (declare-fun x () Int) (declare-fun y () Int) -- 2.30.2