diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-10 16:48:51 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-10 16:48:51 -0500 |
| commit | adcbee78823120baa47eb8ba868b614512a121a9 (patch) | |
| tree | f019c19fa63cc06c8b4e93df2cbde7d61791368b /test | |
| parent | f29ced85757a85b6bd72b741d6ac7ff45ba29619 (diff) | |
Sygus repair constants (#1812)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/constant-ite-bv.sy | 29 |
2 files changed, 30 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index c3de09de2..52eb63789 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1474,6 +1474,7 @@ REG1_TESTS = \ regress1/sygus/clock-inc-tuple.sy \ regress1/sygus/commutative.sy \ regress1/sygus/constant.sy \ + regress1/sygus/constant-ite-bv.sy \ regress1/sygus/dt-test-ns.sy \ regress1/sygus/dup-op.sy \ regress1/sygus/fg_polynomial3.sy \ diff --git a/test/regress/regress1/sygus/constant-ite-bv.sy b/test/regress/regress1/sygus/constant-ite-bv.sy new file mode 100644 index 000000000..330ef026e --- /dev/null +++ b/test/regress/regress1/sygus/constant-ite-bv.sy @@ -0,0 +1,29 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --no-sygus-pbe --sygus-repair-const +(set-logic BV) +(synth-fun f ( (x (BitVec 64))) (BitVec 64) +( +(Start (BitVec 64) ( + #x0000000000000000 + #x0000000000000001 + x + (bvnot Start) + (bvadd Start Start) + (ite StartBool Start Start) + (Constant (BitVec 64)) + )) +(StartBool Bool ((bvule Start Start))) +) +) +(constraint (= (f #x6E393354DFFAAB51) #xC8E366559002AA57)) +(constraint (= (f #xFDA75AD598A27135) #xC8E366559002AA57)) +(constraint (= (f #x58682C0FA4F8DB6D) #xC8E366559002AA57)) +(constraint (= (f #x58FDC0941A7E079F) #xC8E366559002AA57)) +(constraint (= (f #xBDC9B88103ECB0C9) #xC8E366559002AA57)) +(constraint (= (f #x000000000001502F) #x0000000000000000)) +(constraint (= (f #x0000000000010999) #x0000000000000000)) +(constraint (= (f #x0000000000013169) #x0000000000000000)) +(constraint (= (f #x000000000001B1A9) #x0000000000000000)) +(constraint (= (f #x0000000000016D77) #x0000000000000000)) +(constraint (= (f #x0000000000000001) #x0000000000000000)) +(check-synth) |