Fix parsing selectors for nullary constructors in smtlib 2.6 format.

2 files changed, 30 insertions, 1 deletions

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index caf1fc61c..b437f1878 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -80,7 +80,8 @@ TESTS =	\
 	dt-param-2.6.smt2 \
 	dt-color-2.6.smt2 \
 	dt-match-pat-param-2.6.smt2 \
-	tuple-no-clash.cvc
+	tuple-no-clash.cvc \
+	jsat-2.6.smt2
 
 FAILING_TESTS = \
 	datatype-dump.cvc
diff --git a/test/regress/regress0/datatypes/jsat-2.6.smt2 b/test/regress/regress0/datatypes/jsat-2.6.smt2
new file mode 100644
index 000000000..7e7fe4f49
--- /dev/null
+++ b/test/regress/regress0/datatypes/jsat-2.6.smt2
@@ -0,0 +1,28 @@
+; COMMAND-LINE: --lang=smt2.6
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero))
+((cons (car tree) (cdr list)) (null))
+((node (children list)) (leaf (data nat)))
+))
+(declare-fun x1 () nat)
+(declare-fun x2 () nat)
+(declare-fun x3 () nat)
+(declare-fun x4 () nat)
+(declare-fun x5 () nat)
+(declare-fun x6 () list)
+(declare-fun x7 () list)
+(declare-fun x8 () list)
+(declare-fun x9 () list)
+(declare-fun x10 () list)
+(declare-fun x11 () tree)
+(declare-fun x12 () tree)
+(declare-fun x13 () tree)
+(declare-fun x14 () tree)
+(declare-fun x15 () tree)
+
+(assert (and (and (= x9 x7) ((_ is node) x11)) (not ((_ is zero) x5))))
+(check-sat)
+
+