diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-12-19 11:58:52 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-12-19 11:58:52 -0600 |
| commit | 6b46621c4076ace3b0703e29fbdadca04f7635cb (patch) | |
| tree | b9d46b8d2453fac49e119fa22811ad610195cca6 /test/regress | |
| parent | f6f26013ce73db50502dc5452c08e304ab2e3ac3 (diff) | |
Fix issues with REWRITE_DONE in floating point rewriter (#2762)
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy | 26 |
2 files changed, 27 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 95e4b8875..0b196855f 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1640,6 +1640,7 @@ set(regress_1_tests regress1/sygus/sygus-lambda-fv.sy regress1/sygus/sygus-uf-ex.sy regress1/sygus/t8.sy + regress1/sygus/temp_input_to_synth_ic-error-121418.sy regress1/sygus/tl-type-0.sy regress1/sygus/tl-type-4x.sy regress1/sygus/tl-type.sy diff --git a/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy b/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy new file mode 100644 index 000000000..4efd90314 --- /dev/null +++ b/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy @@ -0,0 +1,26 @@ +; REQUIRES: symfpu +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic ALL) +(define-sort FP () (_ FloatingPoint 3 5)) +(synth-fun IC ((t FP)) Bool + ((Start Bool ( + true + false + (fp.isZero StartFP) + (ite Start Start Start) + )) + (StartFP FP ( + t + (fp.sub StartRM StartFP StartFP) + (fp.max StartFP StartFP) + )) + (StartRM RoundingMode + (RNE)) +)) + +(constraint (not (IC (fp #b0 #b110 #b1001) ))) +(constraint (not (IC (fp #b1 #b101 #b1101) ))) +(constraint (not (IC (fp #b1 #b001 #b0110) ))) +(constraint (IC (fp #b0 #b001 #b0001) )) +(check-synth) |