From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 1 May 2020 00:59:45 +0000 (-0500)
Subject: Fix regression (#4424)
X-Git-Tag: cvc5-1.0.0~3326
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2799fd28155ef85aba68c90bc65fe52f529cdd7e;p=cvc5.git

Fix regression (#4424)

Fixes regress1.
---

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)