Minor

ajreynol · Jan 15, 2025 · 1d04a1d · 1d04a1d
1 parent fc8bcae
commit 1d04a1d
Show file tree

Hide file tree

Showing 3 changed files with 1 addition and 15 deletions.
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
@@ -1024,7 +1024,6 @@ set(regress_0_tests
   regress0/ite2.smt2
   regress0/ite3.smt2
   regress0/ite4.smt2
-  regress0/lambda-shadow-sem.smt2
   regress0/lang_opts_2_6_1.smt2
   regress0/lemmas/clocksynchro_5clocks.main_invar.base.model.smtv1.smt2
   regress0/lemmas/fs_not_sc_seen.induction.smtv1.smt2

diff --git a/test/regress/cli/regress0/lambda-shadow-sem.smt2 b/test/regress/cli/regress0/lambda-shadow-sem.smt2
diff --git a/test/regress/cli/regress0/proofs/define-fun-shadow.smt2 b/test/regress/cli/regress0/proofs/define-fun-shadow.smt2
@@ -1,8 +1,4 @@
-; DISABLE-TESTER: dump
-; REQUIRES: no-competition
-; SCRUBBER: grep -o "All formal arguments to defined functions must be unique"
-; EXPECT: All formal arguments to defined functions must be unique
-; EXIT: 1
+; EXPECT: unsat
 (set-logic ALL)
 (declare-const x2 Bool)
 (define-fun s ((a Int) (b Int) (z Int) (z Int)) Bool (= 0 0))