From 7d27cae34c7c3cda9a7827754fb5b8e485d515db Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 11 Apr 2019 13:06:08 -0500
Subject:  Eliminate Boolean ITE within terms, fixes 2947 (#2949)

---
 test/regress/regress0/uf/issue2947.smt2 | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test/regress/regress0/uf/issue2947.smt2

(limited to 'test/regress/regress0')

diff --git a/test/regress/regress0/uf/issue2947.smt2 b/test/regress/regress0/uf/issue2947.smt2
new file mode 100644
index 000000000..6bb60b9d7
--- /dev/null
+++ b/test/regress/regress0/uf/issue2947.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_UF)
+(set-info :status unsat)
+(declare-fun f (Bool) Bool)
+(assert
+  (not (f true))
+)
+(assert
+  (f (ite (f true) true (f false)))
+)
+(check-sat)
+(exit)
-- 
cgit v1.2.3