From 716ce9168d846ea991f8404a78aeb1ccccfbce14 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 2 May 2018 20:25:09 -0500 Subject: Initial support for string standard in smt lib 2.6 (#1848) --- test/regress/regress1/strings/issue1105.smt2 | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'test/regress/regress1/strings/issue1105.smt2') diff --git a/test/regress/regress1/strings/issue1105.smt2 b/test/regress/regress1/strings/issue1105.smt2 index 81e7672da..bf5cb7669 100644 --- a/test/regress/regress1/strings/issue1105.smt2 +++ b/test/regress/regress1/strings/issue1105.smt2 @@ -1,9 +1,10 @@ +(set-info :smt-lib-version 2.5) (set-logic ALL) (set-option :strings-exp true) (set-info :status sat) -(declare-datatype Val ( +(declare-datatypes () ((Val (Str (str String)) - (Num (num Int)))) + (Num (num Int))))) (declare-const var0 Val) (assert (=> (is-Str var0) (distinct (str.to.int (str var0)) (- 1)))) -- cgit v1.2.3