From 0b351ea67e8f58165bc7773b23cc52f5dea8066d Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Thu, 18 Mar 2021 14:14:24 -0400
Subject: [PATCH] test: add regression test for bad LRA preprocessing

---
 tests/unsat/reg_lra_2_ite.smt2 | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 tests/unsat/reg_lra_2_ite.smt2

diff --git a/tests/unsat/reg_lra_2_ite.smt2 b/tests/unsat/reg_lra_2_ite.smt2
new file mode 100644
index 00000000..117820b5
--- /dev/null
+++ b/tests/unsat/reg_lra_2_ite.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_LRA)
+(set-info :status unsat)
+(declare-fun x_39 () Bool)
+(declare-fun x_83 () Bool)
+(assert (not (<= (ite x_39 0.0 0.0) (ite x_83 0.0 0.0))))
+(check-sat)
+(exit)