From 2799fd28155ef85aba68c90bc65fe52f529cdd7e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 30 Apr 2020 19:59:45 -0500 Subject: [PATCH] Fix regression (#4424) Fixes regress1. --- test/regress/regress1/strings/pre_ctn_no_skolem_share.smt2 | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/test/regress/regress1/strings/pre_ctn_no_skolem_share.smt2 b/test/regress/regress1/strings/pre_ctn_no_skolem_share.smt2 index 277a14df8..87c7a8de7 100644 --- a/test/regress/regress1/strings/pre_ctn_no_skolem_share.smt2 +++ b/test/regress/regress1/strings/pre_ctn_no_skolem_share.smt2 @@ -1,5 +1,7 @@ (set-info :smt-lib-version 2.6) (set-logic ALL) +(set-option :strings-exp true) +(set-option :strings-fmf true) (set-info :status sat) (declare-fun z () String) (declare-fun n () Int) @@ -15,4 +17,3 @@ ))) (check-sat) -(get-model) -- 2.30.2