From 4612dd66cee87b7d4b735b416785d539083757fa Mon Sep 17 00:00:00 2001
From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Mon, 23 Sep 2013 16:54:32 -0500
Subject: adds model generation for strings, and a hacked way in arith engine
 for models

---
 test/regress/regress0/strings/Makefile.am   |  1 +
 test/regress/regress0/strings/model001.smt2 | 12 ++++++++++++
 2 files changed, 13 insertions(+)
 create mode 100644 test/regress/regress0/strings/model001.smt2

(limited to 'test/regress')

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 269ec49ed..699a7ff3c 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -25,6 +25,7 @@ TESTS =	\
   str003.smt2 \
   str004.smt2 \
   str005.smt2 \
+  model001.smt2 \
   loop001.smt2
 # loop002.smt2 \
 # loop003.smt2 \
diff --git a/test/regress/regress0/strings/model001.smt2 b/test/regress/regress0/strings/model001.smt2
new file mode 100644
index 000000000..e4e35f40d
--- /dev/null
+++ b/test/regress/regress0/strings/model001.smt2
@@ -0,0 +1,12 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :produce-models true)
+
+(declare-fun x () String)
+(declare-fun y () String)
+
+(assert (not (= x y)))
+(assert (= (str.len x) (str.len y)))
+
+(check-sat)
+;(get-model)
-- 
cgit v1.2.3