Fix global-declarations support (#3403)

2 files changed, 30 insertions, 0 deletions

diff --git a/test/regress/regress0/datatypes/bug597-rbt.smt2 b/test/regress/regress0/datatypes/bug597-rbt.smt2
index 078fa59f7..236865aa3 100644
--- a/test/regress/regress0/datatypes/bug597-rbt.smt2
+++ b/test/regress/regress0/datatypes/bug597-rbt.smt2
@@ -1,3 +1,4 @@
+(set-option :global-declarations true)
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
 
diff --git a/test/regress/regress0/smtlib/global-decls.smt2 b/test/regress/regress0/smtlib/global-decls.smt2
new file mode 100644
index 000000000..a8b6c17b2
--- /dev/null
+++ b/test/regress/regress0/smtlib/global-decls.smt2
@@ -0,0 +1,29 @@
+; COMMAND-LINE: --incremental
+(set-option :global-declarations true)
+(set-logic QF_UFDTLIA)
+
+(push 1)
+(declare-datatype Struct1 (par (T0) ((mk-struct1 (struct1-proj0 T0)))))
+(declare-datatypes ((Unit 0)) (((u))))
+(declare-datatypes ((Tree 0)) (((node (data Int) (color Bool) (left Tree) (right Tree)) (nil))))
+(declare-fun x () (Struct1 Bool))
+(declare-sort U1 0)
+(declare-sort U2 1)
+(pop 1)
+
+(assert (= x x))
+
+(define-fun y () (Struct1 Bool) (mk-struct1 true))
+(declare-const z Unit)
+(assert (= u u))
+(assert (is-mk-struct1 y))
+(assert (is-u z))
+
+(declare-fun size (Tree) Int)
+(assert (= (size nil) 0))
+
+(declare-const w1 U1)
+(declare-const w2 (U2 Bool))
+
+(set-info :status sat)
+(check-sat)