From 0d83eb48cdec63e03649d69eb5dca25fcdf98d87 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 6 Dec 2021 12:27:11 -0600 Subject: [PATCH] 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. --- test/regress/CMakeLists.txt | 7 ++ .../regress0/datatypes/proj-issue172.smt2 | 7 ++ test/regress/regress1/proj-issue175.smt2 | 83 +++++++++++++++++++ test/regress/regress1/sets/proj-issue164.smt2 | 10 +++ test/regress/regress1/sets/proj-issue178.smt2 | 10 +++ .../regress/regress1/sygus/proj-issue181.smt2 | 8 ++ .../regress/regress1/sygus/proj-issue183.smt2 | 20 +++++ .../regress/regress1/sygus/proj-issue185.smt2 | 12 +++ 8 files changed, 157 insertions(+) create mode 100644 test/regress/regress0/datatypes/proj-issue172.smt2 create mode 100644 test/regress/regress1/proj-issue175.smt2 create mode 100644 test/regress/regress1/sets/proj-issue164.smt2 create mode 100644 test/regress/regress1/sets/proj-issue178.smt2 create mode 100644 test/regress/regress1/sygus/proj-issue181.smt2 create mode 100644 test/regress/regress1/sygus/proj-issue183.smt2 create mode 100644 test/regress/regress1/sygus/proj-issue185.smt2 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 4169036ba..5afff3246 100644 --- 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 index 000000000..f9f5a2ffc --- /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 index 000000000..2df1e21e6 --- /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 index 000000000..5e343156e --- /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 index 000000000..2b95f43c9 --- /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 index 000000000..656d1e757 --- /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 index 000000000..e50e035f3 --- /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 index 000000000..a3e4b8205 --- /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) -- 2.30.2