From a93c19459811f9cdd651958c0b01fa8a441e19ec Mon Sep 17 00:00:00 2001
From: Philipp Ruemmer <ph_r@gmx.net>
Date: Tue, 16 Jul 2024 16:32:05 +0200
Subject: [PATCH] fix bug #55, raise an error for ill-formed clauses

---
 regression-tests/horn-smt-lib/Answers              | 4 ++++
 regression-tests/horn-smt-lib/illformed.smt2       | 9 +++++++++
 regression-tests/horn-smt-lib/runtests             | 3 ++-
 src/main/scala/lazabs/horn/parser/HornReader.scala | 4 +++-
 4 files changed, 18 insertions(+), 2 deletions(-)
 create mode 100644 regression-tests/horn-smt-lib/illformed.smt2

diff --git a/regression-tests/horn-smt-lib/Answers b/regression-tests/horn-smt-lib/Answers
index 1c9f3e98..9729ec43 100644
--- a/regression-tests/horn-smt-lib/Answers
+++ b/regression-tests/horn-smt-lib/Answers
@@ -358,3 +358,7 @@ Warning: ignoring exit
 unsat
 
 0: FALSE
+
+illformed.smt2
+Warning: ignoring get-model
+(error "Uninterpreted functions or constants in clauses are not supported")
diff --git a/regression-tests/horn-smt-lib/illformed.smt2 b/regression-tests/horn-smt-lib/illformed.smt2
new file mode 100644
index 00000000..325a50c1
--- /dev/null
+++ b/regression-tests/horn-smt-lib/illformed.smt2
@@ -0,0 +1,9 @@
+; Input that should be rejected, no Horn clauses
+
+(set-logic UFLIA)
+(declare-fun n () Int)
+
+(assert (and (> n 1) (not (= (- n 1) 1))))
+
+(check-sat)
+(get-model)
\ No newline at end of file
diff --git a/regression-tests/horn-smt-lib/runtests b/regression-tests/horn-smt-lib/runtests
index 4f73c65c..198dd3a3 100755
--- a/regression-tests/horn-smt-lib/runtests
+++ b/regression-tests/horn-smt-lib/runtests
@@ -20,7 +20,8 @@ TESTS="mccarthy91.nts.smt2 \
        clause-shortener-bug.smt2 \
        extract.smt2 \
        solution-verifier-bug.smt2 \
-       groebner-bug.smt2"
+       groebner-bug.smt2 \
+       illformed.smt2"
 
 for name in $TESTS; do
     echo
diff --git a/src/main/scala/lazabs/horn/parser/HornReader.scala b/src/main/scala/lazabs/horn/parser/HornReader.scala
index 7f9d8168..b2e7a652 100644
--- a/src/main/scala/lazabs/horn/parser/HornReader.scala
+++ b/src/main/scala/lazabs/horn/parser/HornReader.scala
@@ -423,9 +423,11 @@ class SMTHornReader protected[parser] (
 
     if (ContainsSymbol(clause, (x:IExpression) => x match {
           case IFunApp(f, _) => !(TheoryRegistry lookupSymbol f).isDefined
+          case IConstant(_) => true
           case _ => false
         }))
-      throw new Exception ("Uninterpreted functions are not supported")
+      throw new Exception (
+        "Uninterpreted functions or constants in clauses are not supported")
 
     clause =
       if (elimArrays) {