8 files changed, 79 insertions, 1 deletions
diff --git a/test/regress/regress0/aufbv/issue3687-check-models-small.smt2 b/test/regress/regress0/aufbv/issue3687-check-models-small.smt2
new file mode 100644
index 000000000..88cbd8a0b
--- /dev/null
+++ b/test/regress/regress0/aufbv/issue3687-check-models-small.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --check-models
+; EXPECT: sat
+(set-logic QF_AUFBV)
+(declare-fun a () (Array (_ BitVec 2) (_ BitVec 2)))
+(declare-fun b () (_ BitVec 2))
+(assert (distinct #b01 (select (store (store a #b01 (bvor #b01 (select a
+  #b00))) #b10 #b00) b)))
+(check-sat)
+\ No newline at end of file
diff --git a/test/regress/regress0/bv/bv_to_int_5281.smt2 b/test/regress/regress0/bv/bv_to_int_5281.smt2
index 4d0da1dbb..dc2cb7f35 100644
--- a/test/regress/regress0/bv/bv_to_int_5281.smt2
+++ b/test/regress/regress0/bv/bv_to_int_5281.smt2
@@ -1,4 +1,4 @@
-; COMMAND: --check-models --incremental
+; COMMAND-LINE: --check-models --incremental
 ; EXPECT: sat
 (set-logic ALL)
 (set-option :check-models true)
diff --git a/test/regress/regress0/issue4707-bv-to-bool-small.smt2 b/test/regress/regress0/issue4707-bv-to-bool-small.smt2
new file mode 100644
index 000000000..c2f0a58ad
--- /dev/null
+++ b/test/regress/regress0/issue4707-bv-to-bool-small.smt2
@@ -0,0 +1,13 @@
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun b () (Array (_ BitVec 10) (_ BitVec 1)))
+(declare-fun c () (Array (_ BitVec 10) (_ BitVec 1)))
+(declare-fun ae () (_ BitVec 10))
+(declare-fun ag () (_ BitVec 10))
+(declare-fun ak () (_ BitVec 10))
+(assert (= (_ bv1 1) (bvand (bvcomp ae ((_ zero_extend 9) (select b (_ bv0
+  10)))) (bvsdiv (bvcomp ae ak) (bvand (ite (= (_ bv0 1) (bvcomp ag (bvshl ((_
+  zero_extend 9) (select c (bvadd ae (_ bv3 10)))) (_ bv8 10)))) (_ bv1 1) (_
+  bv0 1)) (ite (= b (store (store c (bvadd ae (_ bv3 10)) ((_ extract 0 0)
+  (bvlshr ag (_ bv8 10)))) ak (_ bv1 1))) (_ bv1 1) (_ bv0 1)))))))
+(check-sat)
+\ No newline at end of file
diff --git a/test/regress/regress0/issue5099-model-1.smt2 b/test/regress/regress0/issue5099-model-1.smt2
new file mode 100644
index 000000000..dd422ab3b
--- /dev/null
+++ b/test/regress/regress0/issue5099-model-1.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: -m
+; EXPECT: sat
+; EXPECT: ((baz true))
+(set-logic QF_NIRA)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(assert (! (or (= a (div 0 b))) :named baz))
+(assert (and (> b 5)))
+(check-sat)
+(get-assignment)
diff --git a/test/regress/regress0/issue5099-model-2.smt2 b/test/regress/regress0/issue5099-model-2.smt2
new file mode 100644
index 000000000..2bd27093f
--- /dev/null
+++ b/test/regress/regress0/issue5099-model-2.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: -m
+; EXPECT: sat
+; EXPECT: ((IP true))
+(set-logic QF_NRA)
+(declare-const r11 Real)
+(declare-const r16 Real)
+(assert (! (distinct (/ 1 r16) r11) :named IP))
+(check-sat)
+(get-assignment)
+\ No newline at end of file
diff --git a/test/regress/regress0/issue5540-2-dump-model.smt2 b/test/regress/regress0/issue5540-2-dump-model.smt2
new file mode 100644
index 000000000..56d3b2458
--- /dev/null
+++ b/test/regress/regress0/issue5540-2-dump-model.smt2
@@ -0,0 +1,9 @@
+; SCRUBBER: sed -e 's/Bool.*$/Bool/'
+; COMMAND-LINE: --dump-models
+; EXPECT: sat
+; EXPECT: (
+; EXPECT: (define-fun v16 () Bool
+; EXPECT: )
+(set-logic UFLIA)
+(declare-fun v16 () Bool)
+(check-sat)
diff --git a/test/regress/regress0/issue5540-model-decls.smt2 b/test/regress/regress0/issue5540-model-decls.smt2
new file mode 100644
index 000000000..714159c9f
--- /dev/null
+++ b/test/regress/regress0/issue5540-model-decls.smt2
@@ -0,0 +1,19 @@
+; SCRUBBER: sed -e 's/Bool.*$/Bool/'
+; COMMAND-LINE: --dump-models -i
+; EXPECT:sat
+; EXPECT: (
+; EXPECT: (define-fun a () Bool
+; EXPECT: )
+; EXPECT: sat
+; EXPECT: (
+; EXPECT: (define-fun a () Bool
+; EXPECT: )
+; EXPECT: sat
+; EXPECT: (
+; EXPECT: (define-fun a () Bool
+; EXPECT: )
+(set-logic ALL)
+(declare-fun a () Bool)
+(check-sat)
+(check-sat)
+(check-sat)
diff --git a/test/regress/regress0/strings/leq.smt2 b/test/regress/regress0/strings/leq.smt2
new file mode 100644
index 000000000..b3bd40739
--- /dev/null
+++ b/test/regress/regress0/strings/leq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --strings-exp
+(set-logic QF_SLIA)
+(declare-const x String)
+(declare-const y String)
+(assert (or
+  (not (str.<= (str.++ "A" x) (str.++ "B" y)))
+  (not (str.<= (str.++ "A" x) (str.++ "BC" y)))
+  (str.<= (str.++ "A" "D" x) (str.++ "AC" y))))
+(set-info :status unsat)
+(check-sat)