fix bug #55, raise an error for ill-formed clauses

uuverifiers · Jul 16, 2024 · a93c194 · a93c194
1 parent 3384e46
commit a93c194
Show file tree

Hide file tree

Showing 4 changed files with 18 additions and 2 deletions.
diff --git 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
@@ -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)
diff --git 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
@@ -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) {