diff --git a/plutus-tx-plugin/plutus-tx-plugin.cabal b/plutus-tx-plugin/plutus-tx-plugin.cabal
index 97e56d91a1a..a47c4b4f2ab 100644
--- a/plutus-tx-plugin/plutus-tx-plugin.cabal
+++ b/plutus-tx-plugin/plutus-tx-plugin.cabal
@@ -128,6 +128,7 @@ test-suite plutus-tx-plugin-tests
     Blueprint.Tests.Lib
     Blueprint.Tests.Lib.AsData.Blueprint
     Blueprint.Tests.Lib.AsData.Decls
+    Budget.BuiltinAndLib
     Budget.Spec
     Budget.WithGHCOptimisations
     Budget.WithoutGHCOptimisations
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_AllTrue.golden.eval b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_AllTrue.golden.eval
new file mode 100644
index 00000000000..aa7c4cf8901
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_AllTrue.golden.eval
@@ -0,0 +1,6 @@
+CPU:                   919_970
+Memory:                  5_003
+AST Size:                   63
+Flat Size:                  91
+
+(con unit ())
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_AllTrue.golden.pir b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_AllTrue.golden.pir
new file mode 100644
index 00000000000..0393e454c69
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_AllTrue.golden.pir
@@ -0,0 +1,26 @@
+(let
+    data Unit | Unit_match where
+      Unit : Unit
+  in
+  \(x : integer) (y : integer) (z : integer) ->
+    let
+      !b : bool = lessThanInteger x 100
+      !b : bool = lessThanInteger y 100
+      !b : bool = lessThanInteger z 100
+      !b : bool
+        = case (unit -> bool) b [(\(ds : unit) -> False), (\(ds : unit) -> b)]
+            ()
+    in
+    case
+      (unit -> unit)
+      (case (unit -> bool) b [(\(ds : unit) -> False), (\(ds : unit) -> b)] ())
+      [ (\(ds : unit) ->
+           let
+             !x : Unit = trace {Unit} "conditions not met" Unit
+           in
+           error {unit})
+      , (\(ds : unit) -> ()) ]
+      ())
+  50
+  60
+  70
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_AllTrue.golden.uplc b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_AllTrue.golden.uplc
new file mode 100644
index 00000000000..ea5f34b977d
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_AllTrue.golden.uplc
@@ -0,0 +1,21 @@
+(program
+   1.1.0
+   ((\x y z ->
+       (\b ->
+          (\b ->
+             (\b ->
+                (\b ->
+                   case
+                     (case b [(\ds -> False), (\ds -> b)] ())
+                     [ (\ds ->
+                          (\x -> error)
+                            (force trace "conditions not met" (constr 0 [])))
+                     , (\ds -> ()) ]
+                     ())
+                  (case b [(\ds -> False), (\ds -> b)] ()))
+               (lessThanInteger z 100))
+            (lessThanInteger y 100))
+         (lessThanInteger x 100))
+      50
+      60
+      70))
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_EarlyFail.golden.eval b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_EarlyFail.golden.eval
new file mode 100644
index 00000000000..1c1ef919814
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_EarlyFail.golden.eval
@@ -0,0 +1,3 @@
+An error has occurred:
+The machine terminated because of an error, either from a built-in function or from an explicit use of 'error'.
+Caused by: error
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_EarlyFail.golden.pir b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_EarlyFail.golden.pir
new file mode 100644
index 00000000000..e9d6e61c90d
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_EarlyFail.golden.pir
@@ -0,0 +1,26 @@
+(let
+    data Unit | Unit_match where
+      Unit : Unit
+  in
+  \(x : integer) (y : integer) (z : integer) ->
+    let
+      !b : bool = lessThanInteger x 100
+      !b : bool = lessThanInteger y 100
+      !b : bool = lessThanInteger z 100
+      !b : bool
+        = case (unit -> bool) b [(\(ds : unit) -> False), (\(ds : unit) -> b)]
+            ()
+    in
+    case
+      (unit -> unit)
+      (case (unit -> bool) b [(\(ds : unit) -> False), (\(ds : unit) -> b)] ())
+      [ (\(ds : unit) ->
+           let
+             !x : Unit = trace {Unit} "conditions not met" Unit
+           in
+           error {unit})
+      , (\(ds : unit) -> ()) ]
+      ())
+  150
+  60
+  70
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_EarlyFail.golden.uplc b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_EarlyFail.golden.uplc
new file mode 100644
index 00000000000..6c49f60c3e9
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_EarlyFail.golden.uplc
@@ -0,0 +1,21 @@
+(program
+   1.1.0
+   ((\x y z ->
+       (\b ->
+          (\b ->
+             (\b ->
+                (\b ->
+                   case
+                     (case b [(\ds -> False), (\ds -> b)] ())
+                     [ (\ds ->
+                          (\x -> error)
+                            (force trace "conditions not met" (constr 0 [])))
+                     , (\ds -> ()) ]
+                     ())
+                  (case b [(\ds -> False), (\ds -> b)] ()))
+               (lessThanInteger z 100))
+            (lessThanInteger y 100))
+         (lessThanInteger x 100))
+      150
+      60
+      70))
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_LateFail.golden.eval b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_LateFail.golden.eval
new file mode 100644
index 00000000000..1c1ef919814
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_LateFail.golden.eval
@@ -0,0 +1,3 @@
+An error has occurred:
+The machine terminated because of an error, either from a built-in function or from an explicit use of 'error'.
+Caused by: error
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_LateFail.golden.pir b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_LateFail.golden.pir
new file mode 100644
index 00000000000..5cfd9b5f6b6
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_LateFail.golden.pir
@@ -0,0 +1,26 @@
+(let
+    data Unit | Unit_match where
+      Unit : Unit
+  in
+  \(x : integer) (y : integer) (z : integer) ->
+    let
+      !b : bool = lessThanInteger x 100
+      !b : bool = lessThanInteger y 100
+      !b : bool = lessThanInteger z 100
+      !b : bool
+        = case (unit -> bool) b [(\(ds : unit) -> False), (\(ds : unit) -> b)]
+            ()
+    in
+    case
+      (unit -> unit)
+      (case (unit -> bool) b [(\(ds : unit) -> False), (\(ds : unit) -> b)] ())
+      [ (\(ds : unit) ->
+           let
+             !x : Unit = trace {Unit} "conditions not met" Unit
+           in
+           error {unit})
+      , (\(ds : unit) -> ()) ]
+      ())
+  50
+  60
+  150
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_LateFail.golden.uplc b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_LateFail.golden.uplc
new file mode 100644
index 00000000000..08a0e5fa87d
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAndIfError_LateFail.golden.uplc
@@ -0,0 +1,21 @@
+(program
+   1.1.0
+   ((\x y z ->
+       (\b ->
+          (\b ->
+             (\b ->
+                (\b ->
+                   case
+                     (case b [(\ds -> False), (\ds -> b)] ())
+                     [ (\ds ->
+                          (\x -> error)
+                            (force trace "conditions not met" (constr 0 [])))
+                     , (\ds -> ()) ]
+                     ())
+                  (case b [(\ds -> False), (\ds -> b)] ()))
+               (lessThanInteger z 100))
+            (lessThanInteger y 100))
+         (lessThanInteger x 100))
+      50
+      60
+      150))
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_AllTrue.golden.eval b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_AllTrue.golden.eval
new file mode 100644
index 00000000000..b0f708bf7ba
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_AllTrue.golden.eval
@@ -0,0 +1,6 @@
+CPU:                   839_970
+Memory:                  4_503
+AST Size:                   48
+Flat Size:                  58
+
+(con bool True)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_AllTrue.golden.pir b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_AllTrue.golden.pir
new file mode 100644
index 00000000000..1260e122f74
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_AllTrue.golden.pir
@@ -0,0 +1,12 @@
+(\(x : integer) (y : integer) (z : integer) ->
+   let
+     !b : bool = lessThanInteger x 100
+     !b : bool = lessThanInteger y 100
+     !b : bool = lessThanInteger z 100
+     !b : bool
+       = case (unit -> bool) b [(\(ds : unit) -> False), (\(ds : unit) -> b)] ()
+   in
+   case (unit -> bool) b [(\(ds : unit) -> False), (\(ds : unit) -> b)] ())
+  50
+  60
+  70
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_AllTrue.golden.uplc b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_AllTrue.golden.uplc
new file mode 100644
index 00000000000..9f6cb67fe83
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_AllTrue.golden.uplc
@@ -0,0 +1,14 @@
+(program
+   1.1.0
+   ((\x y z ->
+       (\b ->
+          (\b ->
+             (\b ->
+                (\b -> case b [(\ds -> False), (\ds -> b)] ())
+                  (case b [(\ds -> False), (\ds -> b)] ()))
+               (lessThanInteger z 100))
+            (lessThanInteger y 100))
+         (lessThanInteger x 100))
+      50
+      60
+      70))
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_EarlyFail.golden.eval b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_EarlyFail.golden.eval
new file mode 100644
index 00000000000..9b57ad84739
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_EarlyFail.golden.eval
@@ -0,0 +1,6 @@
+CPU:                   839_970
+Memory:                  4_503
+AST Size:                   48
+Flat Size:                  59
+
+(con bool False)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_EarlyFail.golden.pir b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_EarlyFail.golden.pir
new file mode 100644
index 00000000000..547c7036e7e
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_EarlyFail.golden.pir
@@ -0,0 +1,12 @@
+(\(x : integer) (y : integer) (z : integer) ->
+   let
+     !b : bool = lessThanInteger x 100
+     !b : bool = lessThanInteger y 100
+     !b : bool = lessThanInteger z 100
+     !b : bool
+       = case (unit -> bool) b [(\(ds : unit) -> False), (\(ds : unit) -> b)] ()
+   in
+   case (unit -> bool) b [(\(ds : unit) -> False), (\(ds : unit) -> b)] ())
+  150
+  60
+  70
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_EarlyFail.golden.uplc b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_EarlyFail.golden.uplc
new file mode 100644
index 00000000000..54c5c249949
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_EarlyFail.golden.uplc
@@ -0,0 +1,14 @@
+(program
+   1.1.0
+   ((\x y z ->
+       (\b ->
+          (\b ->
+             (\b ->
+                (\b -> case b [(\ds -> False), (\ds -> b)] ())
+                  (case b [(\ds -> False), (\ds -> b)] ()))
+               (lessThanInteger z 100))
+            (lessThanInteger y 100))
+         (lessThanInteger x 100))
+      150
+      60
+      70))
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_LateFail.golden.eval b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_LateFail.golden.eval
new file mode 100644
index 00000000000..1baea9b709c
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_LateFail.golden.eval
@@ -0,0 +1,6 @@
+CPU:                   839_970
+Memory:                  4_503
+AST Size:                   48
+Flat Size:                  58
+
+(con bool False)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_LateFail.golden.pir b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_LateFail.golden.pir
new file mode 100644
index 00000000000..f20df0f58e4
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_LateFail.golden.pir
@@ -0,0 +1,12 @@
+(\(x : integer) (y : integer) (z : integer) ->
+   let
+     !b : bool = lessThanInteger x 100
+     !b : bool = lessThanInteger y 100
+     !b : bool = lessThanInteger z 100
+     !b : bool
+       = case (unit -> bool) b [(\(ds : unit) -> False), (\(ds : unit) -> b)] ()
+   in
+   case (unit -> bool) b [(\(ds : unit) -> False), (\(ds : unit) -> b)] ())
+  50
+  60
+  150
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_LateFail.golden.uplc b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_LateFail.golden.uplc
new file mode 100644
index 00000000000..447da1b8347
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinAnd_LateFail.golden.uplc
@@ -0,0 +1,14 @@
+(program
+   1.1.0
+   ((\x y z ->
+       (\b ->
+          (\b ->
+             (\b ->
+                (\b -> case b [(\ds -> False), (\ds -> b)] ())
+                  (case b [(\ds -> False), (\ds -> b)] ()))
+               (lessThanInteger z 100))
+            (lessThanInteger y 100))
+         (lessThanInteger x 100))
+      50
+      60
+      150))
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_AllTrue.golden.eval b/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_AllTrue.golden.eval
new file mode 100644
index 00000000000..3da9c9adeb1
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_AllTrue.golden.eval
@@ -0,0 +1,6 @@
+CPU:                   727_970
+Memory:                  3_803
+AST Size:                   67
+Flat Size:                 133
+
+(con unit ())
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_AllTrue.golden.pir b/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_AllTrue.golden.pir
new file mode 100644
index 00000000000..be78734dbc1
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_AllTrue.golden.pir
@@ -0,0 +1,38 @@
+(let
+    data Unit | Unit_match where
+      Unit : Unit
+  in
+  \(x : integer) (y : integer) (z : integer) ->
+    case
+      (unit -> unit)
+      (lessThanInteger x 100)
+      [ (\(ds : unit) ->
+           let
+             !x : Unit = trace {Unit} "conditions not met" Unit
+           in
+           error {unit})
+      , (\(ds : unit) ->
+           case
+             (unit -> unit)
+             (lessThanInteger y 100)
+             [ (\(ds : unit) ->
+                  let
+                    !x : Unit = trace {Unit} "conditions not met" Unit
+                  in
+                  error {unit})
+             , (\(ds : unit) ->
+                  case
+                    (unit -> unit)
+                    (lessThanInteger z 100)
+                    [ (\(ds : unit) ->
+                         let
+                           !x : Unit = trace {Unit} "conditions not met" Unit
+                         in
+                         error {unit})
+                    , (\(ds : unit) -> ()) ]
+                    ()) ]
+             ()) ]
+      ())
+  50
+  60
+  70
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_AllTrue.golden.uplc b/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_AllTrue.golden.uplc
new file mode 100644
index 00000000000..3fbe0c76e6d
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_AllTrue.golden.uplc
@@ -0,0 +1,26 @@
+(program
+   1.1.0
+   ((\x y z ->
+       case
+         (lessThanInteger x 100)
+         [ (\ds ->
+              (\x -> error) (force trace "conditions not met" (constr 0 [])))
+         , (\ds ->
+              case
+                (lessThanInteger y 100)
+                [ (\ds ->
+                     (\x -> error)
+                       (force trace "conditions not met" (constr 0 [])))
+                , (\ds ->
+                     case
+                       (lessThanInteger z 100)
+                       [ (\ds ->
+                            (\x -> error)
+                              (force trace "conditions not met" (constr 0 [])))
+                       , (\ds -> ()) ]
+                       ()) ]
+                ()) ]
+         ())
+      50
+      60
+      70))
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_EarlyFail.golden.eval b/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_EarlyFail.golden.eval
new file mode 100644
index 00000000000..1c1ef919814
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_EarlyFail.golden.eval
@@ -0,0 +1,3 @@
+An error has occurred:
+The machine terminated because of an error, either from a built-in function or from an explicit use of 'error'.
+Caused by: error
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_EarlyFail.golden.pir b/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_EarlyFail.golden.pir
new file mode 100644
index 00000000000..3e7a579e5ca
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_EarlyFail.golden.pir
@@ -0,0 +1,38 @@
+(let
+    data Unit | Unit_match where
+      Unit : Unit
+  in
+  \(x : integer) (y : integer) (z : integer) ->
+    case
+      (unit -> unit)
+      (lessThanInteger x 100)
+      [ (\(ds : unit) ->
+           let
+             !x : Unit = trace {Unit} "conditions not met" Unit
+           in
+           error {unit})
+      , (\(ds : unit) ->
+           case
+             (unit -> unit)
+             (lessThanInteger y 100)
+             [ (\(ds : unit) ->
+                  let
+                    !x : Unit = trace {Unit} "conditions not met" Unit
+                  in
+                  error {unit})
+             , (\(ds : unit) ->
+                  case
+                    (unit -> unit)
+                    (lessThanInteger z 100)
+                    [ (\(ds : unit) ->
+                         let
+                           !x : Unit = trace {Unit} "conditions not met" Unit
+                         in
+                         error {unit})
+                    , (\(ds : unit) -> ()) ]
+                    ()) ]
+             ()) ]
+      ())
+  150
+  60
+  70
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_EarlyFail.golden.uplc b/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_EarlyFail.golden.uplc
new file mode 100644
index 00000000000..7f376ec979e
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_EarlyFail.golden.uplc
@@ -0,0 +1,26 @@
+(program
+   1.1.0
+   ((\x y z ->
+       case
+         (lessThanInteger x 100)
+         [ (\ds ->
+              (\x -> error) (force trace "conditions not met" (constr 0 [])))
+         , (\ds ->
+              case
+                (lessThanInteger y 100)
+                [ (\ds ->
+                     (\x -> error)
+                       (force trace "conditions not met" (constr 0 [])))
+                , (\ds ->
+                     case
+                       (lessThanInteger z 100)
+                       [ (\ds ->
+                            (\x -> error)
+                              (force trace "conditions not met" (constr 0 [])))
+                       , (\ds -> ()) ]
+                       ()) ]
+                ()) ]
+         ())
+      150
+      60
+      70))
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_LateFail.golden.eval b/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_LateFail.golden.eval
new file mode 100644
index 00000000000..1c1ef919814
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_LateFail.golden.eval
@@ -0,0 +1,3 @@
+An error has occurred:
+The machine terminated because of an error, either from a built-in function or from an explicit use of 'error'.
+Caused by: error
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_LateFail.golden.pir b/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_LateFail.golden.pir
new file mode 100644
index 00000000000..cb4dda78005
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_LateFail.golden.pir
@@ -0,0 +1,38 @@
+(let
+    data Unit | Unit_match where
+      Unit : Unit
+  in
+  \(x : integer) (y : integer) (z : integer) ->
+    case
+      (unit -> unit)
+      (lessThanInteger x 100)
+      [ (\(ds : unit) ->
+           let
+             !x : Unit = trace {Unit} "conditions not met" Unit
+           in
+           error {unit})
+      , (\(ds : unit) ->
+           case
+             (unit -> unit)
+             (lessThanInteger y 100)
+             [ (\(ds : unit) ->
+                  let
+                    !x : Unit = trace {Unit} "conditions not met" Unit
+                  in
+                  error {unit})
+             , (\(ds : unit) ->
+                  case
+                    (unit -> unit)
+                    (lessThanInteger z 100)
+                    [ (\(ds : unit) ->
+                         let
+                           !x : Unit = trace {Unit} "conditions not met" Unit
+                         in
+                         error {unit})
+                    , (\(ds : unit) -> ()) ]
+                    ()) ]
+             ()) ]
+      ())
+  50
+  60
+  150
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_LateFail.golden.uplc b/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_LateFail.golden.uplc
new file mode 100644
index 00000000000..9b052189755
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andBuiltinIfNest_LateFail.golden.uplc
@@ -0,0 +1,26 @@
+(program
+   1.1.0
+   ((\x y z ->
+       case
+         (lessThanInteger x 100)
+         [ (\ds ->
+              (\x -> error) (force trace "conditions not met" (constr 0 [])))
+         , (\ds ->
+              case
+                (lessThanInteger y 100)
+                [ (\ds ->
+                     (\x -> error)
+                       (force trace "conditions not met" (constr 0 [])))
+                , (\ds ->
+                     case
+                       (lessThanInteger z 100)
+                       [ (\ds ->
+                            (\x -> error)
+                              (force trace "conditions not met" (constr 0 [])))
+                       , (\ds -> ()) ]
+                       ()) ]
+                ()) ]
+         ())
+      50
+      60
+      150))
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_AllTrue.golden.eval b/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_AllTrue.golden.eval
new file mode 100644
index 00000000000..5a21a5322e1
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_AllTrue.golden.eval
@@ -0,0 +1,6 @@
+CPU:                   647_970
+Memory:                  3_303
+AST Size:                   36
+Flat Size:                  48
+
+(con bool True)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_AllTrue.golden.pir b/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_AllTrue.golden.pir
new file mode 100644
index 00000000000..57d9d33288d
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_AllTrue.golden.pir
@@ -0,0 +1,20 @@
+(let
+    !ifThenElse : all a. bool -> a -> a -> a
+      = /\a -> \(b : bool) (x : a) (y : a) -> case a b [y, x]
+  in
+  \(x : integer) (y : integer) (z : integer) ->
+    ifThenElse
+      {unit -> bool}
+      (lessThanInteger x 100)
+      (\(ds : unit) ->
+         ifThenElse
+           {unit -> bool}
+           (lessThanInteger y 100)
+           (\(ds : unit) -> lessThanInteger z 100)
+           (\(ds : unit) -> False)
+           ())
+      (\(ds : unit) -> False)
+      ())
+  50
+  60
+  70
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_AllTrue.golden.uplc b/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_AllTrue.golden.uplc
new file mode 100644
index 00000000000..bf373dc6d78
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_AllTrue.golden.uplc
@@ -0,0 +1,15 @@
+(program
+   1.1.0
+   ((\x y z ->
+       case
+         (lessThanInteger x 100)
+         [ (\ds -> False)
+         , (\ds ->
+              case
+                (lessThanInteger y 100)
+                [(\ds -> False), (\ds -> lessThanInteger z 100)]
+                ()) ]
+         ())
+      50
+      60
+      70))
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_EarlyFail.golden.eval b/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_EarlyFail.golden.eval
new file mode 100644
index 00000000000..e49af1b625c
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_EarlyFail.golden.eval
@@ -0,0 +1,6 @@
+CPU:                   349_390
+Memory:                  2_001
+AST Size:                   36
+Flat Size:                  49
+
+(con bool False)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_EarlyFail.golden.pir b/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_EarlyFail.golden.pir
new file mode 100644
index 00000000000..a009c0e0c66
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_EarlyFail.golden.pir
@@ -0,0 +1,20 @@
+(let
+    !ifThenElse : all a. bool -> a -> a -> a
+      = /\a -> \(b : bool) (x : a) (y : a) -> case a b [y, x]
+  in
+  \(x : integer) (y : integer) (z : integer) ->
+    ifThenElse
+      {unit -> bool}
+      (lessThanInteger x 100)
+      (\(ds : unit) ->
+         ifThenElse
+           {unit -> bool}
+           (lessThanInteger y 100)
+           (\(ds : unit) -> lessThanInteger z 100)
+           (\(ds : unit) -> False)
+           ())
+      (\(ds : unit) -> False)
+      ())
+  150
+  60
+  70
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_EarlyFail.golden.uplc b/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_EarlyFail.golden.uplc
new file mode 100644
index 00000000000..0c226be28c4
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_EarlyFail.golden.uplc
@@ -0,0 +1,15 @@
+(program
+   1.1.0
+   ((\x y z ->
+       case
+         (lessThanInteger x 100)
+         [ (\ds -> False)
+         , (\ds ->
+              case
+                (lessThanInteger y 100)
+                [(\ds -> False), (\ds -> lessThanInteger z 100)]
+                ()) ]
+         ())
+      150
+      60
+      70))
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_LateFail.golden.eval b/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_LateFail.golden.eval
new file mode 100644
index 00000000000..bf50421c37f
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_LateFail.golden.eval
@@ -0,0 +1,6 @@
+CPU:                   647_970
+Memory:                  3_303
+AST Size:                   36
+Flat Size:                  48
+
+(con bool False)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_LateFail.golden.pir b/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_LateFail.golden.pir
new file mode 100644
index 00000000000..7eee7851135
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_LateFail.golden.pir
@@ -0,0 +1,20 @@
+(let
+    !ifThenElse : all a. bool -> a -> a -> a
+      = /\a -> \(b : bool) (x : a) (y : a) -> case a b [y, x]
+  in
+  \(x : integer) (y : integer) (z : integer) ->
+    ifThenElse
+      {unit -> bool}
+      (lessThanInteger x 100)
+      (\(ds : unit) ->
+         ifThenElse
+           {unit -> bool}
+           (lessThanInteger y 100)
+           (\(ds : unit) -> lessThanInteger z 100)
+           (\(ds : unit) -> False)
+           ())
+      (\(ds : unit) -> False)
+      ())
+  50
+  60
+  150
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_LateFail.golden.uplc b/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_LateFail.golden.uplc
new file mode 100644
index 00000000000..ffc990ef415
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andDirectIfThenElse_LateFail.golden.uplc
@@ -0,0 +1,15 @@
+(program
+   1.1.0
+   ((\x y z ->
+       case
+         (lessThanInteger x 100)
+         [ (\ds -> False)
+         , (\ds ->
+              case
+                (lessThanInteger y 100)
+                [(\ds -> False), (\ds -> lessThanInteger z 100)]
+                ()) ]
+         ())
+      50
+      60
+      150))
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andLazy_AllTrue.golden.eval b/plutus-tx-plugin/test/Budget/9.6/andLazy_AllTrue.golden.eval
new file mode 100644
index 00000000000..10c518d1851
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andLazy_AllTrue.golden.eval
@@ -0,0 +1,6 @@
+CPU:                   551_970
+Memory:                  2_703
+AST Size:                   28
+Flat Size:                  42
+
+(con bool True)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andLazy_AllTrue.golden.pir b/plutus-tx-plugin/test/Budget/9.6/andLazy_AllTrue.golden.pir
new file mode 100644
index 00000000000..ca7f3c716f6
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andLazy_AllTrue.golden.pir
@@ -0,0 +1,15 @@
+(\(x : integer) (y : integer) (z : integer) ->
+   case
+     (all dead. bool)
+     (lessThanInteger x 100)
+     [ (/\dead -> False)
+     , (/\dead ->
+          case
+            (all dead. bool)
+            (lessThanInteger y 100)
+            [(/\dead -> False), (/\dead -> lessThanInteger z 100)]
+            {all dead. dead}) ]
+     {all dead. dead})
+  50
+  60
+  70
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andLazy_AllTrue.golden.uplc b/plutus-tx-plugin/test/Budget/9.6/andLazy_AllTrue.golden.uplc
new file mode 100644
index 00000000000..16ade09f407
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andLazy_AllTrue.golden.uplc
@@ -0,0 +1,10 @@
+(program
+   1.1.0
+   ((\x y z ->
+       case
+         (lessThanInteger x 100)
+         [ False
+         , (case (lessThanInteger y 100) [False, (lessThanInteger z 100)]) ])
+      50
+      60
+      70))
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andLazy_EarlyFail.golden.eval b/plutus-tx-plugin/test/Budget/9.6/andLazy_EarlyFail.golden.eval
new file mode 100644
index 00000000000..ed6a97525d5
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andLazy_EarlyFail.golden.eval
@@ -0,0 +1,6 @@
+CPU:                   301_390
+Memory:                  1_701
+AST Size:                   28
+Flat Size:                  43
+
+(con bool False)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andLazy_EarlyFail.golden.pir b/plutus-tx-plugin/test/Budget/9.6/andLazy_EarlyFail.golden.pir
new file mode 100644
index 00000000000..6874d1e6115
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andLazy_EarlyFail.golden.pir
@@ -0,0 +1,15 @@
+(\(x : integer) (y : integer) (z : integer) ->
+   case
+     (all dead. bool)
+     (lessThanInteger x 100)
+     [ (/\dead -> False)
+     , (/\dead ->
+          case
+            (all dead. bool)
+            (lessThanInteger y 100)
+            [(/\dead -> False), (/\dead -> lessThanInteger z 100)]
+            {all dead. dead}) ]
+     {all dead. dead})
+  150
+  60
+  70
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andLazy_EarlyFail.golden.uplc b/plutus-tx-plugin/test/Budget/9.6/andLazy_EarlyFail.golden.uplc
new file mode 100644
index 00000000000..5f116a71cf9
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andLazy_EarlyFail.golden.uplc
@@ -0,0 +1,10 @@
+(program
+   1.1.0
+   ((\x y z ->
+       case
+         (lessThanInteger x 100)
+         [ False
+         , (case (lessThanInteger y 100) [False, (lessThanInteger z 100)]) ])
+      150
+      60
+      70))
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andLazy_LateFail.golden.eval b/plutus-tx-plugin/test/Budget/9.6/andLazy_LateFail.golden.eval
new file mode 100644
index 00000000000..fcafbe5c828
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andLazy_LateFail.golden.eval
@@ -0,0 +1,6 @@
+CPU:                   551_970
+Memory:                  2_703
+AST Size:                   28
+Flat Size:                  42
+
+(con bool False)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andLazy_LateFail.golden.pir b/plutus-tx-plugin/test/Budget/9.6/andLazy_LateFail.golden.pir
new file mode 100644
index 00000000000..18f79ad06d4
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andLazy_LateFail.golden.pir
@@ -0,0 +1,15 @@
+(\(x : integer) (y : integer) (z : integer) ->
+   case
+     (all dead. bool)
+     (lessThanInteger x 100)
+     [ (/\dead -> False)
+     , (/\dead ->
+          case
+            (all dead. bool)
+            (lessThanInteger y 100)
+            [(/\dead -> False), (/\dead -> lessThanInteger z 100)]
+            {all dead. dead}) ]
+     {all dead. dead})
+  50
+  60
+  150
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andLazy_LateFail.golden.uplc b/plutus-tx-plugin/test/Budget/9.6/andLazy_LateFail.golden.uplc
new file mode 100644
index 00000000000..fe0ec234db4
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andLazy_LateFail.golden.uplc
@@ -0,0 +1,10 @@
+(program
+   1.1.0
+   ((\x y z ->
+       case
+         (lessThanInteger x 100)
+         [ False
+         , (case (lessThanInteger y 100) [False, (lessThanInteger z 100)]) ])
+      50
+      60
+      150))
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_AllTrue.golden.eval b/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_AllTrue.golden.eval
new file mode 100644
index 00000000000..29b42522772
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_AllTrue.golden.eval
@@ -0,0 +1,6 @@
+CPU:                   583_970
+Memory:                  2_903
+AST Size:                   31
+Flat Size:                  46
+
+(con bool True)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_AllTrue.golden.pir b/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_AllTrue.golden.pir
new file mode 100644
index 00000000000..ae83bb3c42d
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_AllTrue.golden.pir
@@ -0,0 +1,24 @@
+(let
+    !ifThenElse : all a. bool -> a -> a -> a
+      = /\a -> \(b : bool) (x : a) (y : a) -> case a b [y, x]
+  in
+  \(x : integer) (y : integer) (z : integer) ->
+    case
+      (all dead. bool)
+      (ifThenElse {bool} (lessThanInteger x 100) False True)
+      [ (/\dead ->
+           case
+             (all dead. bool)
+             (ifThenElse {bool} (lessThanInteger y 100) False True)
+             [ (/\dead ->
+                  case
+                    bool
+                    (ifThenElse {bool} (lessThanInteger z 100) False True)
+                    [True, False])
+             , (/\dead -> False) ]
+             {all dead. dead})
+      , (/\dead -> False) ]
+      {all dead. dead})
+  50
+  60
+  70
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_AllTrue.golden.uplc b/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_AllTrue.golden.uplc
new file mode 100644
index 00000000000..864fa7e9ce1
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_AllTrue.golden.uplc
@@ -0,0 +1,12 @@
+(program
+   1.1.0
+   ((\x y z ->
+       case
+         (lessThanInteger x 100)
+         [ False
+         , (case
+              (lessThanInteger y 100)
+              [False, (case (lessThanInteger z 100) [False, True])]) ])
+      50
+      60
+      70))
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_EarlyFail.golden.eval b/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_EarlyFail.golden.eval
new file mode 100644
index 00000000000..0c6045e51e7
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_EarlyFail.golden.eval
@@ -0,0 +1,6 @@
+CPU:                   301_390
+Memory:                  1_701
+AST Size:                   31
+Flat Size:                  47
+
+(con bool False)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_EarlyFail.golden.pir b/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_EarlyFail.golden.pir
new file mode 100644
index 00000000000..e592c1802a5
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_EarlyFail.golden.pir
@@ -0,0 +1,24 @@
+(let
+    !ifThenElse : all a. bool -> a -> a -> a
+      = /\a -> \(b : bool) (x : a) (y : a) -> case a b [y, x]
+  in
+  \(x : integer) (y : integer) (z : integer) ->
+    case
+      (all dead. bool)
+      (ifThenElse {bool} (lessThanInteger x 100) False True)
+      [ (/\dead ->
+           case
+             (all dead. bool)
+             (ifThenElse {bool} (lessThanInteger y 100) False True)
+             [ (/\dead ->
+                  case
+                    bool
+                    (ifThenElse {bool} (lessThanInteger z 100) False True)
+                    [True, False])
+             , (/\dead -> False) ]
+             {all dead. dead})
+      , (/\dead -> False) ]
+      {all dead. dead})
+  150
+  60
+  70
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_EarlyFail.golden.uplc b/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_EarlyFail.golden.uplc
new file mode 100644
index 00000000000..4a61e7fdbe5
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_EarlyFail.golden.uplc
@@ -0,0 +1,12 @@
+(program
+   1.1.0
+   ((\x y z ->
+       case
+         (lessThanInteger x 100)
+         [ False
+         , (case
+              (lessThanInteger y 100)
+              [False, (case (lessThanInteger z 100) [False, True])]) ])
+      150
+      60
+      70))
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_LateFail.golden.eval b/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_LateFail.golden.eval
new file mode 100644
index 00000000000..91f0e6b6626
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_LateFail.golden.eval
@@ -0,0 +1,6 @@
+CPU:                   583_970
+Memory:                  2_903
+AST Size:                   31
+Flat Size:                  46
+
+(con bool False)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_LateFail.golden.pir b/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_LateFail.golden.pir
new file mode 100644
index 00000000000..b10cd6b8cfd
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_LateFail.golden.pir
@@ -0,0 +1,24 @@
+(let
+    !ifThenElse : all a. bool -> a -> a -> a
+      = /\a -> \(b : bool) (x : a) (y : a) -> case a b [y, x]
+  in
+  \(x : integer) (y : integer) (z : integer) ->
+    case
+      (all dead. bool)
+      (ifThenElse {bool} (lessThanInteger x 100) False True)
+      [ (/\dead ->
+           case
+             (all dead. bool)
+             (ifThenElse {bool} (lessThanInteger y 100) False True)
+             [ (/\dead ->
+                  case
+                    bool
+                    (ifThenElse {bool} (lessThanInteger z 100) False True)
+                    [True, False])
+             , (/\dead -> False) ]
+             {all dead. dead})
+      , (/\dead -> False) ]
+      {all dead. dead})
+  50
+  60
+  150
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_LateFail.golden.uplc b/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_LateFail.golden.uplc
new file mode 100644
index 00000000000..b8fc215d398
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/9.6/andMultiWayIf_LateFail.golden.uplc
@@ -0,0 +1,12 @@
+(program
+   1.1.0
+   ((\x y z ->
+       case
+         (lessThanInteger x 100)
+         [ False
+         , (case
+              (lessThanInteger y 100)
+              [False, (case (lessThanInteger z 100) [False, True])]) ])
+      50
+      60
+      150))
\ No newline at end of file
diff --git a/plutus-tx-plugin/test/Budget/BuiltinAndLib.hs b/plutus-tx-plugin/test/Budget/BuiltinAndLib.hs
new file mode 100644
index 00000000000..a4f9c58c258
--- /dev/null
+++ b/plutus-tx-plugin/test/Budget/BuiltinAndLib.hs
@@ -0,0 +1,77 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+{-# HLINT ignore "Use const" #-}
+{-# OPTIONS_GHC -fno-full-laziness #-}
+{-# OPTIONS_GHC -fno-ignore-interface-pragmas #-}
+{-# OPTIONS_GHC -fno-omit-interface-pragmas #-}
+{-# OPTIONS_GHC -fno-spec-constr #-}
+{-# OPTIONS_GHC -fno-specialise #-}
+{-# OPTIONS_GHC -fno-strictness #-}
+{-# OPTIONS_GHC -fno-unbox-small-strict-fields #-}
+{-# OPTIONS_GHC -fno-unbox-strict-fields #-}
+{-# OPTIONS_GHC -fplugin-opt PlutusTx.Plugin:conservative-optimisation #-}
+{-# OPTIONS_GHC -fplugin-opt PlutusTx.Plugin:datatypes=BuiltinCasing #-}
+
+{-| Separate module with GHC optimisation flags disabled, matching the flags
+used by Philip DiSarro in PR #7562 (ValidatorOptimized.hs). This ensures
+that INLINE pragmas behave as intended and builtinAnd gets inlined at the
+call site before the plugin compiles, preserving short-circuit semantics. -}
+module Budget.BuiltinAndLib where
+
+import PlutusTx.Bool (Bool (..))
+import PlutusTx.Builtins.Internal qualified as BI
+import PlutusTx.Integer (Integer)
+import PlutusTx.Ord ((<))
+import PlutusTx.Trace (traceError)
+
+{-# INLINE builtinIf #-}
+builtinIf :: Bool -> (BI.BuiltinUnit -> a) -> (BI.BuiltinUnit -> a) -> a
+builtinIf cond t f = BI.ifThenElse cond t f BI.unitval
+
+{-# INLINE builtinAnd #-}
+builtinAnd :: Bool -> Bool -> Bool
+builtinAnd b1 b2 = builtinIf b1 (\_ -> b2) (\_ -> False)
+
+{-# INLINE andBuiltinAndPattern #-}
+andBuiltinAndPattern :: Integer -> Integer -> Integer -> Bool
+andBuiltinAndPattern x y z =
+  builtinAnd (x < 100) (builtinAnd (y < 100) (z < 100))
+
+{-# INLINE andDirectIfThenElsePattern #-}
+andDirectIfThenElsePattern :: Integer -> Integer -> Integer -> Bool
+andDirectIfThenElsePattern x y z =
+  BI.ifThenElse
+    (x < 100)
+    ( \_ ->
+        BI.ifThenElse
+          (y < 100)
+          (\_ -> z < 100)
+          (\_ -> False)
+          BI.unitval
+    )
+    (\_ -> False)
+    BI.unitval
+
+-- | Philip's exact claim: if (builtinAnd a $ builtinAnd b $ builtinAnd c) then X else error
+{-# INLINE andBuiltinAndIfErrorPattern #-}
+andBuiltinAndIfErrorPattern :: Integer -> Integer -> Integer -> BI.BuiltinUnit
+andBuiltinAndIfErrorPattern x y z =
+  builtinIf
+    (builtinAnd (x < 100) (builtinAnd (y < 100) (z < 100)))
+    (\_ -> BI.unitval)
+    (\_ -> traceError "conditions not met")
+
+-- | Equivalent with nested builtinIf (Philip's actual validator pattern)
+{-# INLINE andBuiltinIfNestPattern #-}
+andBuiltinIfNestPattern :: Integer -> Integer -> Integer -> BI.BuiltinUnit
+andBuiltinIfNestPattern x y z =
+  builtinIf
+    (x < 100)
+    ( \_ ->
+        builtinIf
+          (y < 100)
+          (\_ -> builtinIf (z < 100) (\_ -> BI.unitval) (\_ -> traceError "conditions not met"))
+          (\_ -> traceError "conditions not met")
+    )
+    (\_ -> traceError "conditions not met")
diff --git a/plutus-tx-plugin/test/Budget/Spec.hs b/plutus-tx-plugin/test/Budget/Spec.hs
index 8505691ac63..69e6a725ed4 100644
--- a/plutus-tx-plugin/test/Budget/Spec.hs
+++ b/plutus-tx-plugin/test/Budget/Spec.hs
@@ -3,18 +3,26 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE MultiWayIf #-}
 {-# LANGUAGE NegativeLiterals #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
 {-# OPTIONS_GHC -fplugin-opt PlutusTx.Plugin:datatypes=BuiltinCasing #-}
 
+{-# HLINT ignore "Use camelCase" #-}
+{-# HLINT ignore "Use const" #-}
+{-# HLINT ignore "Redundant if" #-}
+
 module Budget.Spec where
 
 import Test.Tasty.Extras
 
+import Budget.BuiltinAndLib qualified as BuiltinAndLib
 import Budget.WithGHCOptimisations qualified as WithGHCOptTest
 import Budget.WithoutGHCOptimisations qualified as WithoutGHCOptTest
 import Data.Set qualified as Set
@@ -27,21 +35,20 @@ import PlutusTx.Foldable qualified as F
 import PlutusTx.IsData qualified as IsData
 import PlutusTx.Lift (liftCodeDef, makeLift)
 import PlutusTx.List qualified as List
+import PlutusTx.Prelude
 import PlutusTx.Prelude qualified as PlutusTx
 import PlutusTx.Show qualified as PlutusTx
 import PlutusTx.TH (compile)
 import PlutusTx.Test
 
-AsData.asData
-  [d|
-    data MaybeD a = JustD a | NothingD
-    |]
+AsData.asData [d|data MaybeD a = JustD a | NothingD|]
 makeLift ''MaybeD
 
 tests :: TestNested
 tests =
-  testNested "Budget" . pure $
-    testNestedGhc
+  testNested "Budget"
+    . pure
+    $ testNestedGhc
       [ goldenBundle' "sum" compiledSum
       , goldenBundle' "anyCheap" compiledAnyCheap
       , goldenBundle' "anyExpensive" compiledAnyExpensive
@@ -102,6 +109,31 @@ tests =
         goldenBundle' "andWithoutGHCOpts" compiledAndWithoutGHCOpts
       , -- With the function definition in the local module
         goldenBundle' "andWithLocal" compiledAndWithLocal
+      , -- && vs builtinAnd vs alternatives: boolean AND chaining budget
+        -- Pattern 1: Standard && (lazy, delay/force)
+        goldenBundle' "andLazy_AllTrue" andLazy_AllTrue
+      , goldenBundle' "andLazy_EarlyFail" andLazy_EarlyFail
+      , goldenBundle' "andLazy_LateFail" andLazy_LateFail
+      , -- Pattern 2: builtinAnd (lambda/unit)
+        goldenBundle' "andBuiltinAnd_AllTrue" andBuiltinAnd_AllTrue
+      , goldenBundle' "andBuiltinAnd_EarlyFail" andBuiltinAnd_EarlyFail
+      , goldenBundle' "andBuiltinAnd_LateFail" andBuiltinAnd_LateFail
+      , -- Pattern 3: Multi-way if (negated guards)
+        goldenBundle' "andMultiWayIf_AllTrue" andMultiWayIf_AllTrue
+      , goldenBundle' "andMultiWayIf_EarlyFail" andMultiWayIf_EarlyFail
+      , goldenBundle' "andMultiWayIf_LateFail" andMultiWayIf_LateFail
+      , -- Pattern 4: Direct BI.ifThenElse chain (manual lambda/unit)
+        goldenBundle' "andDirectIfThenElse_AllTrue" andDirectIfThenElse_AllTrue
+      , goldenBundle' "andDirectIfThenElse_EarlyFail" andDirectIfThenElse_EarlyFail
+      , goldenBundle' "andDirectIfThenElse_LateFail" andDirectIfThenElse_LateFail
+      , -- Pattern 5: Philip's claim — if (builtinAnd a $ builtinAnd b c) then ok else error
+        goldenBundle' "andBuiltinAndIfError_AllTrue" andBuiltinAndIfError_AllTrue
+      , goldenBundle' "andBuiltinAndIfError_EarlyFail" andBuiltinAndIfError_EarlyFail
+      , goldenBundle' "andBuiltinAndIfError_LateFail" andBuiltinAndIfError_LateFail
+      , -- Pattern 6: Nested builtinIf (Philip's actual validator pattern)
+        goldenBundle' "andBuiltinIfNest_AllTrue" andBuiltinIfNest_AllTrue
+      , goldenBundle' "andBuiltinIfNest_EarlyFail" andBuiltinIfNest_EarlyFail
+      , goldenBundle' "andBuiltinIfNest_LateFail" andBuiltinIfNest_LateFail
       ]
 
 compiledSum :: CompiledCode Integer
@@ -617,19 +649,176 @@ matchAsData =
 compiledAndWithGHCOpts :: CompiledCode Bool
 compiledAndWithGHCOpts =
   let code = $$(compile [||WithGHCOptTest.f||])
-   in flip unsafeApplyCode (liftCodeDef (4 :: Integer)) $
-        unsafeApplyCode code (liftCodeDef (4 :: Integer))
+   in flip unsafeApplyCode (liftCodeDef (4 :: Integer))
+        $ unsafeApplyCode code (liftCodeDef (4 :: Integer))
 
 compiledAndWithoutGHCOpts :: CompiledCode Bool
 compiledAndWithoutGHCOpts =
   let code = $$(compile [||WithoutGHCOptTest.f||])
-   in flip unsafeApplyCode (liftCodeDef (4 :: Integer)) $
-        unsafeApplyCode code (liftCodeDef (4 :: Integer))
+   in flip unsafeApplyCode (liftCodeDef (4 :: Integer))
+        $ unsafeApplyCode code (liftCodeDef (4 :: Integer))
 
 compiledAndWithLocal :: CompiledCode Bool
 compiledAndWithLocal =
   let f :: Integer -> Integer -> Bool
       f x y = (PlutusTx.&&) (x PlutusTx.< (3 :: Integer)) (y PlutusTx.< (3 :: Integer))
       code = $$(compile [||f||])
-   in flip unsafeApplyCode (liftCodeDef (4 :: Integer)) $
-        unsafeApplyCode code (liftCodeDef (4 :: Integer))
+   in flip unsafeApplyCode (liftCodeDef (4 :: Integer))
+        $ unsafeApplyCode code (liftCodeDef (4 :: Integer))
+
+------------------------------------------------------------------------
+-- && vs builtinAnd vs alternatives: boolean AND chaining budget
+------------------------------------------------------------------------
+
+-- Pattern 1: Standard && (lazy, delay/force)
+andLazyPattern :: Integer -> Integer -> Integer -> Bool
+andLazyPattern x y z = (x < 100) && ((y < 100) && (z < 100))
+{-# INLINEABLE andLazyPattern #-}
+
+-- Patterns 2 and 4 (builtinAnd, direct BI.ifThenElse) are defined in
+-- Budget.BuiltinAndLib with GHC optimisation flags disabled and INLINE pragmas,
+-- matching Philip DiSarro's approach in PR #7562.
+
+-- Pattern 3: Multi-way if (negated guards)
+andMultiWayIfPattern :: Integer -> Integer -> Integer -> Bool
+andMultiWayIfPattern x y z =
+  if
+    | x >= 100 -> False
+    | y >= 100 -> False
+    | z >= 100 -> False
+    | otherwise -> True
+{-# INLINEABLE andMultiWayIfPattern #-}
+
+-- Test scenarios: AllTrue (50,60,70), EarlyFail (150,60,70), LateFail (50,60,150)
+
+-- Pattern 1: Standard &&
+andLazy_AllTrue :: CompiledCode Bool
+andLazy_AllTrue =
+  $$(compile [||andLazyPattern||])
+    `unsafeApplyCode` liftCodeDef 50
+    `unsafeApplyCode` liftCodeDef 60
+    `unsafeApplyCode` liftCodeDef 70
+
+andLazy_EarlyFail :: CompiledCode Bool
+andLazy_EarlyFail =
+  $$(compile [||andLazyPattern||])
+    `unsafeApplyCode` liftCodeDef 150
+    `unsafeApplyCode` liftCodeDef 60
+    `unsafeApplyCode` liftCodeDef 70
+
+andLazy_LateFail :: CompiledCode Bool
+andLazy_LateFail =
+  $$(compile [||andLazyPattern||])
+    `unsafeApplyCode` liftCodeDef 50
+    `unsafeApplyCode` liftCodeDef 60
+    `unsafeApplyCode` liftCodeDef 150
+
+-- Pattern 2: builtinAnd (from BuiltinAndLib, with -fno-* flags + INLINE)
+andBuiltinAnd_AllTrue :: CompiledCode Bool
+andBuiltinAnd_AllTrue =
+  $$(compile [||BuiltinAndLib.andBuiltinAndPattern||])
+    `unsafeApplyCode` liftCodeDef 50
+    `unsafeApplyCode` liftCodeDef 60
+    `unsafeApplyCode` liftCodeDef 70
+
+andBuiltinAnd_EarlyFail :: CompiledCode Bool
+andBuiltinAnd_EarlyFail =
+  $$(compile [||BuiltinAndLib.andBuiltinAndPattern||])
+    `unsafeApplyCode` liftCodeDef 150
+    `unsafeApplyCode` liftCodeDef 60
+    `unsafeApplyCode` liftCodeDef 70
+
+andBuiltinAnd_LateFail :: CompiledCode Bool
+andBuiltinAnd_LateFail =
+  $$(compile [||BuiltinAndLib.andBuiltinAndPattern||])
+    `unsafeApplyCode` liftCodeDef 50
+    `unsafeApplyCode` liftCodeDef 60
+    `unsafeApplyCode` liftCodeDef 150
+
+-- Pattern 3: Multi-way if
+andMultiWayIf_AllTrue :: CompiledCode Bool
+andMultiWayIf_AllTrue =
+  $$(compile [||andMultiWayIfPattern||])
+    `unsafeApplyCode` liftCodeDef 50
+    `unsafeApplyCode` liftCodeDef 60
+    `unsafeApplyCode` liftCodeDef 70
+
+andMultiWayIf_EarlyFail :: CompiledCode Bool
+andMultiWayIf_EarlyFail =
+  $$(compile [||andMultiWayIfPattern||])
+    `unsafeApplyCode` liftCodeDef 150
+    `unsafeApplyCode` liftCodeDef 60
+    `unsafeApplyCode` liftCodeDef 70
+
+andMultiWayIf_LateFail :: CompiledCode Bool
+andMultiWayIf_LateFail =
+  $$(compile [||andMultiWayIfPattern||])
+    `unsafeApplyCode` liftCodeDef 50
+    `unsafeApplyCode` liftCodeDef 60
+    `unsafeApplyCode` liftCodeDef 150
+
+-- Pattern 4: Direct BI.ifThenElse (from BuiltinAndLib, with -fno-* flags + INLINE)
+andDirectIfThenElse_AllTrue :: CompiledCode Bool
+andDirectIfThenElse_AllTrue =
+  $$(compile [||BuiltinAndLib.andDirectIfThenElsePattern||])
+    `unsafeApplyCode` liftCodeDef 50
+    `unsafeApplyCode` liftCodeDef 60
+    `unsafeApplyCode` liftCodeDef 70
+
+andDirectIfThenElse_EarlyFail :: CompiledCode Bool
+andDirectIfThenElse_EarlyFail =
+  $$(compile [||BuiltinAndLib.andDirectIfThenElsePattern||])
+    `unsafeApplyCode` liftCodeDef 150
+    `unsafeApplyCode` liftCodeDef 60
+    `unsafeApplyCode` liftCodeDef 70
+
+andDirectIfThenElse_LateFail :: CompiledCode Bool
+andDirectIfThenElse_LateFail =
+  $$(compile [||BuiltinAndLib.andDirectIfThenElsePattern||])
+    `unsafeApplyCode` liftCodeDef 50
+    `unsafeApplyCode` liftCodeDef 60
+    `unsafeApplyCode` liftCodeDef 150
+
+-- Pattern 5: Philip's claim — if (builtinAnd a $ builtinAnd b c) then ok else error
+andBuiltinAndIfError_AllTrue :: CompiledCode BuiltinUnit
+andBuiltinAndIfError_AllTrue =
+  $$(compile [||BuiltinAndLib.andBuiltinAndIfErrorPattern||])
+    `unsafeApplyCode` liftCodeDef 50
+    `unsafeApplyCode` liftCodeDef 60
+    `unsafeApplyCode` liftCodeDef 70
+
+andBuiltinAndIfError_EarlyFail :: CompiledCode BuiltinUnit
+andBuiltinAndIfError_EarlyFail =
+  $$(compile [||BuiltinAndLib.andBuiltinAndIfErrorPattern||])
+    `unsafeApplyCode` liftCodeDef 150
+    `unsafeApplyCode` liftCodeDef 60
+    `unsafeApplyCode` liftCodeDef 70
+
+andBuiltinAndIfError_LateFail :: CompiledCode BuiltinUnit
+andBuiltinAndIfError_LateFail =
+  $$(compile [||BuiltinAndLib.andBuiltinAndIfErrorPattern||])
+    `unsafeApplyCode` liftCodeDef 50
+    `unsafeApplyCode` liftCodeDef 60
+    `unsafeApplyCode` liftCodeDef 150
+
+-- Pattern 6: Nested builtinIf (Philip's actual validator pattern)
+andBuiltinIfNest_AllTrue :: CompiledCode BuiltinUnit
+andBuiltinIfNest_AllTrue =
+  $$(compile [||BuiltinAndLib.andBuiltinIfNestPattern||])
+    `unsafeApplyCode` liftCodeDef 50
+    `unsafeApplyCode` liftCodeDef 60
+    `unsafeApplyCode` liftCodeDef 70
+
+andBuiltinIfNest_EarlyFail :: CompiledCode BuiltinUnit
+andBuiltinIfNest_EarlyFail =
+  $$(compile [||BuiltinAndLib.andBuiltinIfNestPattern||])
+    `unsafeApplyCode` liftCodeDef 150
+    `unsafeApplyCode` liftCodeDef 60
+    `unsafeApplyCode` liftCodeDef 70
+
+andBuiltinIfNest_LateFail :: CompiledCode BuiltinUnit
+andBuiltinIfNest_LateFail =
+  $$(compile [||BuiltinAndLib.andBuiltinIfNestPattern||])
+    `unsafeApplyCode` liftCodeDef 50
+    `unsafeApplyCode` liftCodeDef 60
+    `unsafeApplyCode` liftCodeDef 150