2 files changed, 91 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 03d38df5e..a04619342 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1804,6 +1804,7 @@ set(regress_1_tests
   regress1/sygus/phone-1-long.sy
   regress1/sygus/planning-unif.sy
   regress1/sygus/process-10-vars.sy
+  regress1/sygus/pLTL_5_trace.sy
   regress1/sygus/qe.sy
   regress1/sygus/qf_abv.smt2
   regress1/sygus/real-any-const.sy
diff --git a/test/regress/regress1/sygus/pLTL_5_trace.sy b/test/regress/regress1/sygus/pLTL_5_trace.sy
new file mode 100644
index 000000000..532a8f3a8
--- /dev/null
+++ b/test/regress/regress1/sygus/pLTL_5_trace.sy
@@ -0,0 +1,90 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --lang=sygus2
+(set-logic BV)
+
+;Trace length 
+(define-sort Stream () (_ BitVec 48))
+(define-fun ZERO () Stream (_ bv0 48))
+(define-fun ONE () Stream (_ bv1 48))
+
+
+(define-fun S_FALSE () Stream ZERO)
+(define-fun S_TRUE () Stream (bvnot S_FALSE))
+
+; Yesterday: X << 1
+(define-fun
+  Y ( (X Stream) ) Stream
+  (bvshl X ONE)
+)
+
+; Once: X|-X
+(define-fun
+  O ( (X Stream) ) Stream
+  (bvor X (bvneg X))
+)
+
+; Historically: X & ~(1 + X)
+(define-fun
+  H ( (X Stream) ) Stream
+  (bvand X (bvnot (bvadd ONE X)))
+)
+
+; Since: Z | (X & ~((X | Z) + Z))
+(define-fun
+S ( (X Stream) (Z Stream) ) Stream
+  (bvor Z
+    (bvand X 
+      (bvnot (bvadd  (bvor X Z) Z ))
+    )
+  )
+)
+
+(define-fun
+  bvimpl ( (X Stream) (Z Stream) ) Stream
+  (bvor (bvnot X) Z)
+)
+
+(synth-fun phi ((ulInformationTransfer Stream) (dlInformationTransfer Stream) (rrcConnectionReconfiguration Stream) (measurementReport Stream) (systemInformationBlockType1 Stream) (securityModeComplete Stream) (systemInformation Stream) (rrcConnectionReestablishmentReject Stream) (rrcConnectionRequest Stream) (rrcConnectionSetupComplete Stream) (rrcConnectionRelease Stream) (ueCapabilityInformation Stream) (rrcConnectionSetup Stream) (securityModeCommand Stream) (ueCapabilityEnquiry Stream) (rrcConnectionReconfigurationComplete Stream) (rrcConnectionReestablishmentRequest Stream)) Stream
+   ((<F> Stream))
+   ((<F> Stream (
+     S_TRUE 
+     S_FALSE
+     ( Variable Stream ) 
+     (bvnot <F>)
+     (bvand <F> <F>) 
+     (bvor <F> <F>)
+     (bvimpl <F> <F>)
+     (Y <F>)
+     (O <F>)
+     (H <F>)
+     (S <F> <F>)
+   )))
+)
+
+;; Positive examples
+;Positive Trace Data
+(constraint
+   (and
+    (= ((_ extract 8 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000100000 #b000000000000000000000000000000000000000011000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000010000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000000000100000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 8 0) S_TRUE))
+    (= (phi #b000000000000000000000100000000100000000000000000 #b000000000000000000000010000000000000000000000000 #b000000101000000001010000000100000100001000100000 #b000000000100000000001000000000000010100000000000 #b000010000001000100000001000000010000000000000000 #b000000000000000000000000000000000000000000010000 #b001100000010111000000000110011000001000000000000 #b100000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000100000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000000010000000 #b000001010000000010100000001000001000010001000000 #b010000000000000000000000000000000000000000000000) S_TRUE)
+    (= ((_ extract 15 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000010000010100000 #b000000000000000000000000000000000001100000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000010000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000001000000000000000 #b000000000000000000000000000000000000010000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000001000000000 #b000000000000000000000000000000000100000101000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 15 0) S_TRUE))
+    (= ((_ extract 15 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000010001000000 #b000000000000000000000000000000000111000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000100000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000001000000000000000 #b000000000000000000000000000000000000001000000000 #b000000000000000000000000000000000000000000001010 #b000000000000000000000000000000000000000000010000 #b000000000000000000000000000000000000000100000000 #b000000000000000000000000000000000000100010000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 15 0) S_TRUE))
+    (= ((_ extract 20 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000001001001010100000 #b000000000000000000000000000000000000100000000000 #b000000000000000000000000000010000100000000000000 #b000000000000000000000000000000000000000000010000 #b000000000000000000000000000001100000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000100000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000010010010101000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 20 0) S_TRUE)) 
+   )
+)
+
+;; Negative examples
+
+;Negative Trace Data
+(constraint
+   (and
+    (not (= ((_ extract 6 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000000000110000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000000000001000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 6 0) S_TRUE)))
+    (not (= ((_ extract 45 0) (phi #b000000000000000000000001000000001000000000000000 #b000000000000000000000000100000000000000000000000 #b000000001010000000010100000001000001000010001000 #b000000000001000000000010000000000000101000000000 #b000000100000010001000000010000000100000000000000 #b000000000000000000000000000000000000000000000000 #b000011000000101110000000001100110000010000000000 #b001000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000001000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000100000 #b000000010100000000101000000010000010000100010000 #b000100000000000000000000000000000000000000000000)) ((_ extract 45 0) S_TRUE)))
+    (not (= ((_ extract 13 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000100000101000 #b000000000000000000000000000000000000011000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000010000000000000 #b000000000000000000000000000000000000000100000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000010000000 #b000000000000000000000000000000000001000001010000 #b000000000000000000000000000000000000000000000000)) ((_ extract 13 0) S_TRUE)))
+    (not (= ((_ extract 13 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000100010000 #b000000000000000000000000000000000001110000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000010000000000000 #b000000000000000000000000000000000000000010000000 #b000000000000000000000000000000000000000000001010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000001000000 #b000000000000000000000000000000000000001000100000 #b000000000000000000000000000000000000000000000000)) ((_ extract 13 0) S_TRUE)))
+    (not (= ((_ extract 18 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000010010010101000 #b000000000000000000000000000000000000001000000000 #b000000000000000000000000000000100001000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000011000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000001000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000100100101010000 #b000000000000000000000000000000000000000000000000)) ((_ extract 18 0) S_TRUE))) 
+   )
+)
+
+; Solution: G (p -> O f) 
+(check-synth)