From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 28 Apr 2017 20:52:17 +0000 (-0500)
Subject: Minor fixes
X-Git-Tag: cvc5-1.0.0~5814
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3ad71136637d0a07b2f24bd83cb9284d312f385d;p=cvc5.git

Minor fixes
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index d73a60ed1..a49190825 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2538,7 +2538,7 @@ indexedFunctionName[CVC4::Expr& op, CVC4::Kind& kind]
     | FP_TO_SBV_TOK m=INTEGER_LITERAL
       { op = MK_CONST(FloatingPointToSBV(AntlrInput::tokenToUnsigned($m))); }
     | TESTER_TOK term[expr, expr2] { 
-        if( expr.getKind()==kind::APPLY_CONSTRUCTOR ){
+        if( expr.getKind()==kind::APPLY_CONSTRUCTOR && expr.getNumChildren()==0 ){
           //for nullary constructors, must get the operator
           expr = expr.getOperator();
         }
diff --git a/test/regress/regress0/nl/real-div-ufnra.smt2 b/test/regress/regress0/nl/real-div-ufnra.smt2
index 5e3b32c40..e7a031fa8 100644
--- a/test/regress/regress0/nl/real-div-ufnra.smt2
+++ b/test/regress/regress0/nl/real-div-ufnra.smt2
@@ -1,7 +1,7 @@
 ; COMMAND-LINE: --nl-ext --simplification=none
 ; EXPECT: sat
 (set-logic QF_UFNRA)
-(set-info :status unsat)
+(set-info :status sat)
 (declare-fun x () Real)
 (declare-fun y () Real)
 (declare-fun f (Real) Real)