Minor fixes

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index d73a60ed1289d3f41354d8b9fb31d24592024ae3..a491908259f773fa4868254ee7adb3f57e953371 100644 (file)
--- 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 5e3b32c4043e7484b3cb0b7fc7b9477603498602..e7a031fa88927ae7d39b476f64a2128436af05db 100644 (file)
--- 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)