From af243d7bd381ddb73b1dd0d9003fdfd8d8ea4587 Mon Sep 17 00:00:00 2001 From: Yoni Zohar Date: Thu, 1 Aug 2024 12:10:02 -0700 Subject: [PATCH] revert --- test/regress/cli/regress0/bv/overflow/saddo1.smt2 | 2 +- test/regress/cli/regress0/bv/overflow/uaddo1.smt2 | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/test/regress/cli/regress0/bv/overflow/saddo1.smt2 b/test/regress/cli/regress0/bv/overflow/saddo1.smt2 index 2fda1ec53ed..4e5bea7f6a7 100644 --- a/test/regress/cli/regress0/bv/overflow/saddo1.smt2 +++ b/test/regress/cli/regress0/bv/overflow/saddo1.smt2 @@ -1,5 +1,5 @@ ; EXPECT: unsat (set-logic QF_BV) (declare-const v (_ BitVec 6)) -(assert (and (bvsgt v (_ bv32 6)) (not (bvsaddo v v)))) +(assert (and (= (bvadd v v) (_ bv53 6)) (not (bvsaddo v v)))) (check-sat) diff --git a/test/regress/cli/regress0/bv/overflow/uaddo1.smt2 b/test/regress/cli/regress0/bv/overflow/uaddo1.smt2 index 0be25004fbf..443ea849ed8 100644 --- a/test/regress/cli/regress0/bv/overflow/uaddo1.smt2 +++ b/test/regress/cli/regress0/bv/overflow/uaddo1.smt2 @@ -1,5 +1,5 @@ ; EXPECT: unsat (set-logic QF_BV) (declare-const v (_ BitVec 6)) -(assert (and (ugt v (_ bv32 6)) (not (bvuaddo v v)))) +(assert (and (= (bvadd v v) (_ bv53 6)) (not (bvuaddo v v)))) (check-sat)