From 5d5a0b81951204b6161837a46624684837945e68 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Tue, 17 Sep 2024 17:13:34 -0500
Subject: [PATCH] [proofs] [alethe] Reenable Alethe regressions and add
 regression from closed issue

---
 test/regress/cli/CMakeLists.txt                 | 16 ++++++++--------
 test/regress/cli/regress0/proofs/issue9927.smt2 |  4 ++++
 2 files changed, 12 insertions(+), 8 deletions(-)
 create mode 100644 test/regress/cli/regress0/proofs/issue9927.smt2

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index aa2bb761353..13acae65115 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -1298,6 +1298,7 @@ set(regress_0_tests
   regress0/printer/tuples_and_records.cvc.smt2
   regress0/proj-issue307-get-value-re.smt2
   regress0/proj-issue645-abs-value-subs.smt2
+  regress0/proofs/alethe-res-need-or-step.smt2
   regress0/proofs/cyclic-ucp.smt2
   regress0/proofs/bvrewrite-concat-merge.smt2
   regress0/proofs/bvrewrite-extract.smt2
@@ -1320,9 +1321,15 @@ set(regress_0_tests
   regress0/proofs/issue9172-doublePropProof.smt2
   regress0/proofs/issue9200-lfsc-inst-sorts.smt2
   regress0/proofs/issue9205-eqProofNary.smt2
+  regress0/proofs/issue9393-optResReconstruction-alethebug.smt2
+  regress0/proofs/issue9515-alethe-skolems-crash.smt2
+  regress0/proofs/issue9516-alethe-skolems-undef-in-proof.smt2
+  regress0/proofs/issue9531-alethe-resolution.smt2
   regress0/proofs/issue9669-clause-level-opt-incremental.smt2
   regress0/proofs/issue9770-open-sat-proof.smt2
+  regress0/proofs/issue9927.smt2
   regress0/proofs/lfsc-test-1.smt2
+  regress0/proofs/nomerge-alethe-pf.smt2
   regress0/proofs/no-proof-uc.smt2
   regress0/proofs/open-pf-datatypes.smt2
   regress0/proofs/open-pf-if-unordered-iff.smt2
@@ -2980,7 +2987,7 @@ set(regress_1_tests
   regress1/seq/proj-issue733-mbqi-w.smt2
   regress1/sets/all1.smt2
   regress1/sets/all2.smt2
-  regress1/sets/all3.smt2  
+  regress1/sets/all3.smt2
   regress1/sets/choose.cvc.smt2
   regress1/sets/choose1.smt2
   regress1/sets/choose2.smt2
@@ -3756,13 +3763,6 @@ set(regress_4_tests
 
 set(regression_disabled_tests
   regress0/arith/miplib-opt1217--27.smtv1.smt2
-  # Alethe tests disabled while fixes to the Alethe backend not fully merged
-  regress0/proofs/alethe-res-need-or-step.smt2
-  regress0/proofs/issue9393-optResReconstruction-alethebug.smt2
-  regress0/proofs/issue9531-alethe-resolution.smt2
-  regress0/proofs/nomerge-alethe-pf.smt2
-  regress0/proofs/issue9515-alethe-skolems-crash.smt2
-  regress0/proofs/issue9516-alethe-skolems-undef-in-proof.smt2
   # unknown on some builds
   regress0/arith/issue7984-quant-trans.smt2
   regress0/aufbv/dubreva005ue.smtv1.smt2
diff --git a/test/regress/cli/regress0/proofs/issue9927.smt2 b/test/regress/cli/regress0/proofs/issue9927.smt2
new file mode 100644
index 00000000000..8371b5657d7
--- /dev/null
+++ b/test/regress/cli/regress0/proofs/issue9927.smt2
@@ -0,0 +1,4 @@
+(set-logic QF_LRA)
+(declare-fun b () Bool)
+(assert (= 0.0 (ite b 2.0 1.0)))
+(check-sat)
\ No newline at end of file