Revert, try enabling regressions

ajreynol · Jan 14, 2025 · a3c73e6 · a3c73e6
1 parent 18bdd46
commit a3c73e6
Show file tree

Hide file tree

Showing 11 changed files with 11 additions and 15 deletions.
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
@@ -229,16 +229,22 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
     ss << "Cannot process term of abstract type " << node;
     throw LogicException(ss.str());
   }
-  if (k == Kind::HO_APPLY)
+  if (k == Kind::HO_APPLY || node.getType().isFunction())
   {
     if (!isHol)
     {
-      if (!node.getType().isFunction())
+      std::stringstream ss;
+      if (k == Kind::HO_APPLY)
       {
-        // If not HO logic, we convert to APPLY_UF
-        Node ret = TheoryUfRewriter::getApplyUfForHoApply(node);
-        return TrustNode::mkTrustRewrite(node, ret);
+        ss << "Higher-order function applications";
       }
+      else
+      {
+        ss << "Function terms";
+      }
+      ss << " are only supported with "
+            "higher-order logic. Try adding the logic prefix HO_.";
+      throw LogicException(ss.str());
     }
   }
   else if (k == Kind::APPLY_UF)

diff --git a/test/regress/cli/regress0/bv/holes/smod-eliminate-fewer-bitwise-ops.smt2 b/test/regress/cli/regress0/bv/holes/smod-eliminate-fewer-bitwise-ops.smt2
@@ -1,4 +1,3 @@
-; DISABLE-TESTER: alethe
 ; EXPECT: unsat
 (set-logic  QF_BV)
 

diff --git a/test/regress/cli/regress0/cores/dd.uc-min-wrong.smt2 b/test/regress/cli/regress0/cores/dd.uc-min-wrong.smt2
@@ -1,4 +1,3 @@
-; DISABLE-TESTER: alethe
 ; COMMAND-LINE: --minimal-unsat-cores
 ; EXPECT: unsat
 (set-logic ALL)

diff --git a/test/regress/cli/regress0/proofs/dd_bug787_beta_reduce.smt2 b/test/regress/cli/regress0/proofs/dd_bug787_beta_reduce.smt2
@@ -1,4 +1,3 @@
-; DISABLE-TESTER: alethe
 ; EXPECT: unsat
 (set-logic ALL)
 (declare-const _vp1-1 (_ BitVec 1))

diff --git a/test/regress/cli/regress0/proofs/dd_fv-bvl.smt2 b/test/regress/cli/regress0/proofs/dd_fv-bvl.smt2
@@ -1,4 +1,3 @@
-; DISABLE-TESTER: alethe
 ; EXPECT: unsat
 (set-logic ALL)
 (define-fun b ((bv (_ BitVec 4))) (_ BitVec 4) bv)

diff --git a/test/regress/cli/regress0/proofs/issue9770-open-sat-proof.smt2 b/test/regress/cli/regress0/proofs/issue9770-open-sat-proof.smt2
@@ -1,4 +1,3 @@
-; DISABLE-TESTER: alethe
 ; EXPECT: unsat
 (set-logic QF_LIA)
 

diff --git a/test/regress/cli/regress1/bv/bug787.smt2 b/test/regress/cli/regress1/bv/bug787.smt2
@@ -1,6 +1,5 @@
 ; COMMAND-LINE: --bitblast=eager 
 ; EXPECT: unsat
-; DISABLE-TESTER: alethe
 (set-logic QF_BV)
 (set-info :status unsat)
 (define-fun hamming-weight ((bv (_ BitVec 4))) (_ BitVec 4)

diff --git a/test/regress/cli/regress1/bv2int-isabelle.smt2 b/test/regress/cli/regress1/bv2int-isabelle.smt2
@@ -1,4 +1,3 @@
-; DISABLE-TESTER: alethe
 ; COMMAND-LINE: --solve-bv-as-int=sum
 ; EXPECT: unsat
 (set-logic ALL)

diff --git a/test/regress/cli/regress1/proofs/add_two_base.smt2 b/test/regress/cli/regress1/proofs/add_two_base.smt2
@@ -1,4 +1,3 @@
-; DISABLE-TESTER: alethe
 ; COMMAND-LINE: --lfsc-flatten --lfsc-expand-trust
 ; EXPECT: unsat
 

diff --git a/test/regress/cli/regress1/quantifiers/example10714-core-no-miniscope-user.smt2 b/test/regress/cli/regress1/quantifiers/example10714-core-no-miniscope-user.smt2
@@ -1,4 +1,3 @@
-; DISABLE-TESTER: alethe	
 ; EXPECT: unsat
 (set-logic ALL)
 (declare-sort integer 0)

diff --git a/test/regress/cli/regress1/quantifiers/proj-issue155.smt2 b/test/regress/cli/regress1/quantifiers/proj-issue155.smt2
@@ -1,4 +1,3 @@
-; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (set-option :miniscope-quant agg)