Fix regression (#4424)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 1 May 2020 00:59:45 +0000 (19:59 -0500)
committerGitHub <noreply@github.com>
Fri, 1 May 2020 00:59:45 +0000 (17:59 -0700)
Fixes regress1.

test/regress/regress1/strings/pre_ctn_no_skolem_share.smt2

index 277a14df8b0cc8606813f58375ce1858ce2883ae..87c7a8de75a1801d29cf6b9aaad749d6a445f586 100644 (file)
@@ -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)