diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-01-10 12:08:16 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-01-10 12:08:16 -0600 |
commit | 3848242e33130ba507cbfcd5d8296cdeaa3dfa35 (patch) | |
tree | 2c7d4de150eb4c09d7aaf112fd8772a53b7565f8 /test | |
parent | 2ac7e8c916bfb33eb73cd90b20a92bef7036ac6b (diff) |
Track trivial cases in transition inference (#3598)
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress1/sygus/abduction_streq.readable.smt2 | 44 |
2 files changed, 45 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index f8608a34d..823bbb0bd 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1727,6 +1727,7 @@ set(regress_1_tests regress1/sygus-abduct-test-user.smt2 regress1/sygus/VC22_a.sy regress1/sygus/abd-simple-conj-4.smt2 + regress1/sygus/abduction_streq.readable.smt2 regress1/sygus/abv.sy regress1/sygus/array_search_5-Q-easy.sy regress1/sygus/bvudiv-by-2.sy diff --git a/test/regress/regress1/sygus/abduction_streq.readable.smt2 b/test/regress/regress1/sygus/abduction_streq.readable.smt2 new file mode 100644 index 000000000..b6a422035 --- /dev/null +++ b/test/regress/regress1/sygus/abduction_streq.readable.smt2 @@ -0,0 +1,44 @@ +; REQUIRES: proof +; COMMAND-LINE: --produce-abducts --sygus-core-connective +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 + +(set-info :smt-lib-version |2.6|) +(set-logic QF_SLIA) +(set-info :source | +Generated by: Andrew Reynolds +Generated on: 2018-04-25 +Generator: Kudzu, converted to v2.6 by CVC4 +Application: Symbolic Execution of Javascript +Target solver: Kaluza +Publications: "A symbolic execution framework for JavaScript" by P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song, 2010. +|) +(set-info :license |"https://creativecommons.org/licenses/by/4.0/"|) +(set-info :category |"industrial"|) +(set-info :status unknown) +(declare-fun I0_2 () Int) +(declare-fun I1_2 () Int) +(declare-fun I2_2 () Int) +(declare-fun PCTEMP_LHS_1 () String) +(declare-fun T1_2 () String) +(declare-fun T2_2 () String) +(declare-fun T3_2 () String) +(declare-fun T_2 () Bool) +(declare-fun T_4 () Bool) +(declare-fun T_5 () Bool) +(declare-fun var_0xINPUT_19 () String) +(assert (= I0_2 (- 5 0))) +(assert (<= 0 0)) +(assert (<= 0 5)) +(assert (<= 5 I1_2)) +(assert (= I2_2 I1_2)) +(assert (= I0_2 (str.len PCTEMP_LHS_1))) +(assert (= var_0xINPUT_19 ( str.++ T1_2 T2_2 ))) +(assert (= T2_2 ( str.++ PCTEMP_LHS_1 T3_2 ))) +(assert (= 0 (str.len T1_2))) +(assert (= I1_2 (str.len var_0xINPUT_19))) +(assert (= T_2 (= PCTEMP_LHS_1 "Hello"))) +(assert T_2) +(assert (= T_4 (= PCTEMP_LHS_1 "hello"))) +(assert (= T_5 (not T_4))) +(get-abduct A T_5) |