Add regressions for fixed projects issues (#7739)

Fixes cvc5/cvc5-projects#164.
Fixes cvc5/cvc5-projects#172.
Fixes cvc5/cvc5-projects#175.
Fixes cvc5/cvc5-projects#178.
Fixes cvc5/cvc5-projects#181.
Fixes cvc5/cvc5-projects#183.
Fixes cvc5/cvc5-projects#185.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 4169036badac4fae7a84642a12f902ebe4ad61b4..5afff3246c91210659400936f8435e8a10a78402 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -511,6 +511,7 @@ set(regress_0_tests
   regress0/datatypes/pair-bool-bool.cvc.smt2
   regress0/datatypes/pair-real-bool.smt2
   regress0/datatypes/parametric-alt-list.cvc.smt2
+  regress0/datatypes/proj-issue172.smt2
   regress0/datatypes/rec1.cvc.smt2
   regress0/datatypes/rec2.cvc.smt2
   regress0/datatypes/rec4.cvc.smt2
@@ -1845,6 +1846,7 @@ set(regress_1_tests
   regress1/nl/tan-rewrite2.smt2
   regress1/nl/zero-subset.smt2
   regress1/non-fatal-errors.smt2
+  regress1/proj-issue175.smt2
   regress1/proof00.smt2
   regress1/proofs/issue6625-unsat-core-proofs.smt2
   regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2
@@ -2218,6 +2220,8 @@ set(regress_1_tests
   regress1/sets/issue5342_difference_version.smt2
   regress1/sets/issue5942-witness.smt2
   regress1/sets/lemmabug-ListElts317minimized.smt2
+  regress1/sets/proj-issue164.smt2
+  regress1/sets/proj-issue178.smt2
   regress1/sets/remove_check_free_31_6.smt2
   regress1/sets/sets-disequal.smt2
   regress1/sets/sets-tuple-poly.cvc.smt2
@@ -2510,6 +2514,9 @@ set(regress_1_tests
   regress1/sygus/phone-1-long.sy
   regress1/sygus/planning-unif.sy
   regress1/sygus/process-10-vars.sy
+  regress1/sygus/proj-issue181.smt2
+  regress1/sygus/proj-issue183.smt2
+  regress1/sygus/proj-issue185.smt2
   regress1/sygus/pLTL_5_trace.sy
   regress1/sygus/qe.sy
   regress1/sygus/qf_abv.smt2

diff --git a/test/regress/regress0/datatypes/proj-issue172.smt2 b/test/regress/regress0/datatypes/proj-issue172.smt2
new file mode 100644 (file)
index 0000000..f9f5a2f
--- /dev/null
+++ b/test/regress/regress0/datatypes/proj-issue172.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-codatatypes ((a 0)) (((b (c Int) (d a)))))
+(declare-fun e () a)
+(declare-fun f () a)
+(assert (= e f))
+(check-sat)

diff --git a/test/regress/regress1/proj-issue175.smt2 b/test/regress/regress1/proj-issue175.smt2
new file mode 100644 (file)
index 0000000..2df1e21
--- /dev/null
+++ b/test/regress/regress1/proj-issue175.smt2
@@ -0,0 +1,83 @@
+(set-logic QF_AUFNIA)
+(set-info :status sat)
+(declare-fun |#offset~STRUCT#?type~INT?length~UINT?off~UINT?data~$Pointer$?input~$Pointer$?comp~$Pointer$#~data| () Int)
+(declare-fun |ssl3_accept_#t~mem38_491| () Int)
+(declare-fun |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~state| () Int)
+(declare-fun ssl3_accept_~s.offset_12 () Int)
+(declare-fun ssl3_accept_~s.base_12 () Int)
+(declare-fun |#memory_int_136| () (Array Int (Array Int Int)))
+(declare-fun |ssl3_accept_#t~mem35_173| () Int)
+(declare-fun |ssl3_accept_#t~mem49_513| () Int)
+(declare-fun |ssl3_accept_#t~mem29_161| () Int)
+(declare-fun |#memory_int_53| () (Array Int (Array Int Int)))
+(declare-fun |ssl3_accept_#t~mem24_68| () Int)
+(declare-fun |#memory_int_601| () (Array Int (Array Int Int)))
+(declare-fun |ssl3_accept_#t~mem31_631| () Int)
+(declare-fun |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~init_num| () Int)
+(declare-fun |#memory_$Pointer$.base_53| () (Array Int (Array Int Int)))
+(declare-fun |#memory_$Pointer$.base_52| () (Array Int (Array Int Int)))
+(declare-fun |ssl3_accept_#t~nondet159_515| () Int)
+(declare-fun ssl3_accept_~ret~10_753 () Int)
+(declare-fun ssl3_accept_~ret~10_314 () Int)
+(declare-fun |ssl3_accept_#t~mem22_459| () Int)
+(declare-fun |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~s3| () Int)
+(declare-fun |#memory_$Pointer$.offset_521| () (Array Int (Array Int Int)))
+(declare-fun |ssl3_accept_#t~mem165.offset_593| () Int)
+(declare-fun |ssl3_accept_#t~mem23_461| () Int)
+(declare-fun |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~packet| () Int)
+(assert
+ (let (($x220 (= |#offset~STRUCT#?type~INT?length~UINT?off~UINT?data~$Pointer$?input~$Pointer$?comp~$Pointer$#~data| 12)))
+ (let (($x2621 (= |ssl3_accept_#t~mem38_491| 8544)))
+ (let (($x2622 (not $x2621)))
+ (let (($x10875 (not $x2622)))
+ (let (($x23085 (and $x10875 $x220)))
+ (not $x23085)))))))
+(assert
+ (let ((?x806 (+ ssl3_accept_~s.offset_12 |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~state|)))
+ (let ((?x1399 (select |#memory_int_136| ssl3_accept_~s.base_12)))
+ (let ((?x1400 (select ?x1399 ?x806)))
+ (let (($x1478 (>= |ssl3_accept_#t~mem35_173| ?x1400)))
+ (not $x1478))))))
+(assert
+ (let (($x2678 (>= |ssl3_accept_#t~mem49_513| 8640)))
+ (not $x2678)))
+(assert
+ (let ((?x806 (+ ssl3_accept_~s.offset_12 |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~state|)))
+ (let ((?x1399 (select |#memory_int_136| ssl3_accept_~s.base_12)))
+ (let ((?x1400 (select ?x1399 ?x806)))
+ (let (($x1447 (<= |ssl3_accept_#t~mem29_161| ?x1400)))
+ (let ((?x1089 (select |#memory_int_53| ssl3_accept_~s.base_12)))
+ (let ((?x1090 (select ?x1089 ?x806)))
+ (let (($x1113 (>= |ssl3_accept_#t~mem24_68| ?x1090)))
+ (let (($x19982 (and $x1113 $x1447)))
+ (not $x19982))))))))))
+(assert
+ (let ((?x806 (+ ssl3_accept_~s.offset_12 |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~state|)))
+ (let ((?x3029 (select |#memory_int_601| ssl3_accept_~s.base_12)))
+ (let ((?x3030 (select ?x3029 ?x806)))
+ (let (($x3088 (>= |ssl3_accept_#t~mem31_631| ?x3030)))
+ (let ((?x1050 (+ ssl3_accept_~s.offset_12 |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~init_num|)))
+ (let ((?x1051 (select |#memory_$Pointer$.base_53| ssl3_accept_~s.base_12)))
+ (let ((?x1032 (select |#memory_$Pointer$.base_52| ssl3_accept_~s.base_12)))
+ (let ((?x1054 (store |#memory_$Pointer$.base_52| ssl3_accept_~s.base_12 (store ?x1032 ?x1050 (select ?x1051 ?x1050)))))
+ (let (($x1055 (= |#memory_$Pointer$.base_53| ?x1054)))
+ (let (($x11490 (and $x1055 $x3088)))
+ (not $x11490))))))))))))
+(assert
+ (let (($x3458 (>= ssl3_accept_~ret~10_753 |ssl3_accept_#t~nondet159_515|)))
+ (let (($x2065 (not (<= ssl3_accept_~ret~10_314 0))))
+ (let (($x50182 (and $x2065 $x3458)))
+ (not $x50182)))))
+(assert
+ (let (($x2542 (not (= |ssl3_accept_#t~mem22_459| 16384))))
+ (let ((?x1068 (+ ssl3_accept_~s.offset_12 |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~s3|)))
+ (let ((?x2719 (select |#memory_$Pointer$.offset_521| ssl3_accept_~s.base_12)))
+ (let ((?x2734 (select ?x2719 ?x1068)))
+ (let (($x2925 (<= |ssl3_accept_#t~mem165.offset_593| ?x2734)))
+ (and $x2925 $x2542)))))))
+(assert
+ (let (($x2547 (not (= |ssl3_accept_#t~mem23_461| 8192))))
+ (let (($x73 (= |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~packet| 72)))
+ (let (($x11452 (and $x73 $x2547)))
+ (not $x11452)))))
+(check-sat)

diff --git a/test/regress/regress1/sets/proj-issue164.smt2 b/test/regress/regress1/sets/proj-issue164.smt2
new file mode 100644 (file)
index 0000000..5e34315
--- /dev/null
+++ b/test/regress/regress1/sets/proj-issue164.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun b () (Set String))
+(declare-fun c () (Set (Tuple Int Int)))
+(declare-fun d () (Set (Tuple Int Int)))
+(declare-fun e () Int)
+(assert (distinct c (set.insert (tuple 0 0) (set.singleton (tuple 1 1)))))
+(assert (distinct d (rel.tclosure c)))
+(assert (distinct e (set.card b)))
+(check-sat)

diff --git a/test/regress/regress1/sets/proj-issue178.smt2 b/test/regress/regress1/sets/proj-issue178.smt2
new file mode 100644 (file)
index 0000000..2b95f43
--- /dev/null
+++ b/test/regress/regress1/sets/proj-issue178.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL)
+(set-info :status sat)
+(set-option :sygus-inference true)
+(set-option :sets-infer-as-lemmas false)
+(declare-fun a () (Set Int))
+(declare-fun b () (Set Int))
+(declare-fun c () (Set Int))
+(declare-fun d () Int)
+(assert (> (set.card (set.minus a (set.inter (set.minus a b) (set.minus a c)))) d))
+(check-sat)

diff --git a/test/regress/regress1/sygus/proj-issue181.smt2 b/test/regress/regress1/sygus/proj-issue181.smt2
new file mode 100644 (file)
index 0000000..656d1e7
--- /dev/null
+++ b/test/regress/regress1/sygus/proj-issue181.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-option :sygus-inference true)
+(set-info :status sat)
+(declare-fun a (Int) Int) 
+(assert (exists ((b Int)) (distinct (a b) (- b  29)))) 
+(assert (distinct (a 0) (- 4))) 
+(assert (= (a (- 99)) (- 107))) 
+(check-sat) 

diff --git a/test/regress/regress1/sygus/proj-issue183.smt2 b/test/regress/regress1/sygus/proj-issue183.smt2
new file mode 100644 (file)
index 0000000..e50e035
--- /dev/null
+++ b/test/regress/regress1/sygus/proj-issue183.smt2
@@ -0,0 +1,20 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(set-option :sygus-inference true)
+(set-info :status sat)
+(declare-fun a () String)
+(declare-fun b () String)
+(declare-const c String)
+(declare-const d String)
+(declare-fun g () Bool)
+(declare-fun e () Bool)
+(declare-fun f () String)
+(assert (str.in_re (str.substr a 0 (str.len (str.substr a 0 (str.len (str.substr a 0 (str.len c)))))) (re.* (re.++ (str.to_re "") (re.* (str.to_re "aa"))))))
+(assert (str.in_re (str.substr b 0 (str.len d)) (re.* (re.++ (re.* (str.to_re "")) (str.to_re "bb")))))
+(assert (= 4 (str.len d)))
+(assert (not (= (str.substr a 0 (str.len c)) d)))
+(assert (= g (not (= "file" (str.substr a (str.len c) (str.len f))))))
+(assert (= e (not g)))
+(assert e)
+(check-sat)  

diff --git a/test/regress/regress1/sygus/proj-issue185.smt2 b/test/regress/regress1/sygus/proj-issue185.smt2
new file mode 100644 (file)
index 0000000..a3e4b82
--- /dev/null
+++ b/test/regress/regress1/sygus/proj-issue185.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: -q
+; EXPECT: unsat
+(set-logic ALL)
+(set-option :sygus-inference true)
+(set-info :status unsat)
+(declare-codatatypes ((a 0)) (((b (c Int) (d a)))))
+(declare-fun e () a)
+(declare-fun f () a)
+(assert (= e (b 0 (b 0 e))))
+(assert (distinct f (b 0 f)))
+(assert (not (distinct e f)))
+(check-sat)