diff --git a/architecture_descriptions/xilinx_ultrascale_plus.yml b/architecture_descriptions/xilinx_ultrascale_plus.yml
index 9a61183e..c8c91881 100644
--- a/architecture_descriptions/xilinx_ultrascale_plus.yml
+++ b/architecture_descriptions/xilinx_ultrascale_plus.yml
@@ -164,7 +164,8 @@ implementations:
       # connectivity or OPMODE value to allow for proper implementation.
       #
       # TODO(@gussmith23): deal with this when we support multiple DSPs.
-      "(not (bveq (extract 5 4 OPMODE) (bv #b01 2)))",
+      # This is the line that we need to get rid of to use PCIN.
+      # "(not (bveq (extract 5 4 OPMODE) (bv #b01 2)))",
 
       # ERROR: [DRC DSPS-4] Invalid PCIN Connection for CARRYINSEL value: DSP48E2 cell DSP48E2_0
       # has CARRYINSEL[2:0] set to 011 which uses the input of the PCIN bus for its computation,
@@ -250,7 +251,7 @@ implementations:
             { name: INMODE, direction: input, bitwidth: 5, value: INMODE },
             { name: MULTSIGNIN, direction: input, bitwidth: 1, value: (bv 0 1) },
             { name: OPMODE, direction: input, bitwidth: 9, value: OPMODE },
-            { name: PCIN, direction: input, bitwidth: 48, value: (bv 0 48) },
+            { name: PCIN, direction: input, bitwidth: 48, value: (choose (zero-extend C (bitvector 48)) (bv 0 48)) },
             { name: RSTA, direction: input, bitwidth: 1, value: (bv 0 1) },
             { name: RSTALLCARRYIN, direction: input, bitwidth: 1, value: (bv 0 1) },
             { name: RSTALUMODE, direction: input, bitwidth: 1, value: (bv 0 1) },
diff --git a/integration_tests/lakeroad/two_stage_multiplier_xilinx.v b/integration_tests/lakeroad/two_stage_multiplier_xilinx.v
index 7e35330f..e806e47c 100644
--- a/integration_tests/lakeroad/two_stage_multiplier_xilinx.v
+++ b/integration_tests/lakeroad/two_stage_multiplier_xilinx.v
@@ -1,5 +1,5 @@
 // RUN: racket $LAKEROAD_DIR/bin/main.rkt \
-// RUN:  --solver bitwuzla \
+// RUN:  --solver cvc5 \
 // RUN:  --verilog-module-filepath %s \
 // RUN:  --architecture xilinx-ultrascale-plus \
 // RUN:  --template dsp \
diff --git a/integration_tests/lakeroad/xilinx_addmuland_1_stage_signed_18_bit.sv b/integration_tests/lakeroad/xilinx_addmuland_1_stage_signed_18_bit.sv
index 7ebef198..7b50922b 100644
--- a/integration_tests/lakeroad/xilinx_addmuland_1_stage_signed_18_bit.sv
+++ b/integration_tests/lakeroad/xilinx_addmuland_1_stage_signed_18_bit.sv
@@ -3,8 +3,8 @@
 // either it wasn't that change, or some other change I did after it just
 // further cemented the breakage.
 //
-// outfile=$(mktemp)
-// RUN: (racket $LAKEROAD_DIR/bin/main.rkt \
+// RUN: outfile=$(mktemp)
+// RUN: racket $LAKEROAD_DIR/bin/main.rkt \
 // RUN:  --solver bitwuzla \
 // RUN:  --verilog-module-filepath %s \
 // RUN:  --architecture xilinx-ultrascale-plus \
@@ -14,44 +14,42 @@
 // RUN:  --verilog-module-out-signal out:18 \
 // RUN:  --pipeline-depth 1 \
 // RUN:  --clock-name clk \
-// RUN:  --module-name top \
+// RUN:  --module-name out \
 // RUN:  --input-signal 'a:(port a 18):18' \
 // RUN:  --input-signal 'b:(port b 18):18' \
 // RUN:  --input-signal 'c:(port c 18):18' \
 // RUN:  --input-signal 'd:(port d 18):18' \
 // RUN:  --timeout 60 \
 // RUN:  --extra-cycles 3 \
-// RUN: || true) 2>&1 \
-// RUN: | FileCheck %s
-//   > $outfile
-//  FileCheck %s < $outfile
-//  if [ -z ${LAKEROAD_PRIVATE_DIR+x} ]; then \
-//    echo "Warning: LAKEROAD_PRIVATE_DIR is not set. Skipping simulation."; \
-//    exit 0; \
-//  else \
-//    python3 $LAKEROAD_DIR/bin/simulate_with_verilator.py \
-//     --use_random_intermediate_inputs \
-//     --seed=23 \
-//     --max_num_tests=10000 \
-//     --verilog_filepath $outfile \
-//     --verilog_filepath %s \
-//     --clock_name clk \
-//     --pipeline_depth 1 \
-//     --output_signal_name out \
-//     --input_signal a:18 \
-//     --input_signal b:18 \
-//     --input_signal c:18 \
-//     --input_signal d:18 \
-//     --verilator_include_dir "$LAKEROAD_PRIVATE_DIR/DSP48E2/" \
-//     --verilator_extra_arg='-DXIL_XECLIB' \
-//     --verilator_extra_arg='-Wno-UNOPTFLAT' \
-//     --verilator_extra_arg='-Wno-LATCH' \
-//     --verilator_extra_arg='-Wno-WIDTH' \
-//     --verilator_extra_arg='-Wno-STMTDLY' \
-//     --verilator_extra_arg='-Wno-CASEX' \
-//     --verilator_extra_arg='-Wno-TIMESCALEMOD' \
-//     --verilator_extra_arg='-Wno-PINMISSING'; \
-//  fi
+// RUN:  > $outfile
+// RUN: FileCheck %s < $outfile
+// RUN: if [ -z ${LAKEROAD_PRIVATE_DIR+x} ]; then \
+// RUN:   echo "Warning: LAKEROAD_PRIVATE_DIR is not set. Skipping simulation."; \
+// RUN:   exit 0; \
+// RUN: else \
+// RUN:   python3 $LAKEROAD_DIR/bin/simulate_with_verilator.py \
+// RUN:    --test_module_name out \
+// RUN:    --ground_truth_module_name top \
+// RUN:    --max_num_tests=10000 \
+// RUN:    --verilog_filepath $outfile \
+// RUN:    --verilog_filepath %s \
+// RUN:    --clock_name clk \
+// RUN:    --pipeline_depth 1 \
+// RUN:    --output_signal out:18 \
+// RUN:    --input_signal a:18 \
+// RUN:    --input_signal b:18 \
+// RUN:    --input_signal c:18 \
+// RUN:    --input_signal d:18 \
+// RUN:    --verilator_include_dir "$LAKEROAD_PRIVATE_DIR/DSP48E2/" \
+// RUN:    --verilator_extra_arg='-DXIL_XECLIB' \
+// RUN:    --verilator_extra_arg='-Wno-UNOPTFLAT' \
+// RUN:    --verilator_extra_arg='-Wno-LATCH' \
+// RUN:    --verilator_extra_arg='-Wno-WIDTH' \
+// RUN:    --verilator_extra_arg='-Wno-STMTDLY' \
+// RUN:    --verilator_extra_arg='-Wno-CASEX' \
+// RUN:    --verilator_extra_arg='-Wno-TIMESCALEMOD' \
+// RUN:    --verilator_extra_arg='-Wno-PINMISSING'; \
+// RUN: fi
 
 (* use_dsp = "yes" *) module top(
 	input signed [17:0] a,
@@ -71,4 +69,4 @@
 	assign out = stage0;
 endmodule
 
-// CHECK: Synthesis Timeout
+// CHECK: module out(a, b, c, clk, d, out);
diff --git a/integration_tests/lakeroad/xilinx_muladd_0_stage_unsigned_13_bit.sv b/integration_tests/lakeroad/xilinx_muladd_0_stage_unsigned_13_bit.sv
index b59f5278..603638bf 100644
--- a/integration_tests/lakeroad/xilinx_muladd_0_stage_unsigned_13_bit.sv
+++ b/integration_tests/lakeroad/xilinx_muladd_0_stage_unsigned_13_bit.sv
@@ -1,6 +1,6 @@
 // RUN: outfile=$(mktemp)
 // RUN: racket $LAKEROAD_DIR/bin/main.rkt \
-// RUN:  --solver stp \
+// RUN:  --solver cvc5 \
 // RUN:  --verilog-module-filepath %s \
 // RUN:  --architecture xilinx-ultrascale-plus \
 // RUN:  --template dsp \
diff --git a/integration_tests/lakeroad/xilinx_mulsub_1_stage_unsigned_14_bit.sv b/integration_tests/lakeroad/xilinx_mulsub_1_stage_unsigned_14_bit.sv
index 96cc44db..59f12ccd 100644
--- a/integration_tests/lakeroad/xilinx_mulsub_1_stage_unsigned_14_bit.sv
+++ b/integration_tests/lakeroad/xilinx_mulsub_1_stage_unsigned_14_bit.sv
@@ -1,6 +1,6 @@
 // RUN: outfile=$(mktemp)
 // RUN: racket $LAKEROAD_DIR/bin/main.rkt \
-// RUN:  --solver bitwuzla \
+// RUN:  --solver cvc5 \
 // RUN:  --verilog-module-filepath %s \
 // RUN:  --architecture xilinx-ultrascale-plus \
 // RUN:  --template dsp \
diff --git a/integration_tests/lakeroad/xilinx_ultrascale_plus_dsp_internal_shift.v b/integration_tests/lakeroad/xilinx_ultrascale_plus_dsp_internal_shift.v
new file mode 100644
index 00000000..e2f2e9e0
--- /dev/null
+++ b/integration_tests/lakeroad/xilinx_ultrascale_plus_dsp_internal_shift.v
@@ -0,0 +1,46 @@
+// RUN: outfile=$(mktemp)
+// RUN: racket $LAKEROAD_DIR/bin/main.rkt \
+// RUN:  --solver bitwuzla \
+// RUN:  --verilog-module-filepath %s \
+// RUN:  --architecture xilinx-ultrascale-plus \
+// RUN:  --template dsp \
+// RUN:  --out-format verilog \
+// RUN:  --top-module-name top \
+// RUN:  --verilog-module-out-signal out:48 \
+// RUN:  --pipeline-depth 0 \
+// RUN:  --module-name out \
+// RUN:  --input-signal 'c:(port c 47):47' \
+// RUN:  --timeout 90 \
+// RUN: > $outfile
+// RUN: FileCheck %s < $outfile
+// RUN: if [ -z ${LAKEROAD_PRIVATE_DIR+x} ]; then \
+// RUN:   echo "Warning: LAKEROAD_PRIVATE_DIR is not set. Skipping simulation."; \
+// RUN:   exit 0; \
+// RUN: else \
+// RUN:   python3 $LAKEROAD_DIR/bin/simulate_with_verilator.py \
+// RUN:    --test_module_name out \
+// RUN:    --ground_truth_module_name top \
+// RUN:    --max_num_tests=10000 \
+// RUN:    --verilog_filepath $outfile \
+// RUN:    --verilog_filepath %s \
+// RUN:    --pipeline_depth 0 \
+// RUN:    --output_signal out:48 \
+// RUN:    --input_signal c:47 \
+// RUN:    --verilator_include_dir "$LAKEROAD_PRIVATE_DIR/DSP48E2/" \
+// RUN:    --verilator_extra_arg='-DXIL_XECLIB' \
+// RUN:    --verilator_extra_arg='-Wno-UNOPTFLAT' \
+// RUN:    --verilator_extra_arg='-Wno-LATCH' \
+// RUN:    --verilator_extra_arg='-Wno-WIDTH' \
+// RUN:    --verilator_extra_arg='-Wno-STMTDLY' \
+// RUN:    --verilator_extra_arg='-Wno-CASEX' \
+// RUN:    --verilator_extra_arg='-Wno-TIMESCALEMOD' \
+// RUN:    --verilator_extra_arg='-Wno-PINMISSING'; \
+// RUN: fi
+
+// TODO(@gussmith23): For some reason, this doesn't work with c of length 48.
+// Works with 47 though.
+module top(input [46:0] c, output [47:0] out);
+  assign out = 48'(48'(c) >> 17);
+endmodule
+
+// CHECK: module out(c, out);
\ No newline at end of file
diff --git a/integration_tests/lakeroad/xilinx_ultrascale_plus_dsp_internal_shift_broken.v b/integration_tests/lakeroad/xilinx_ultrascale_plus_dsp_internal_shift_broken.v
new file mode 100644
index 00000000..62a62795
--- /dev/null
+++ b/integration_tests/lakeroad/xilinx_ultrascale_plus_dsp_internal_shift_broken.v
@@ -0,0 +1,48 @@
+// RUN: outfile=$(mktemp)
+// RUN: (racket $LAKEROAD_DIR/bin/main.rkt \
+// RUN:  --solver bitwuzla \
+// RUN:  --verilog-module-filepath %s \
+// RUN:  --architecture xilinx-ultrascale-plus \
+// RUN:  --template dsp \
+// RUN:  --out-format verilog \
+// RUN:  --top-module-name top \
+// RUN:  --verilog-module-out-signal out:48 \
+// RUN:  --pipeline-depth 0 \
+// RUN:  --module-name out \
+// RUN:  --input-signal 'c:(port c 48):48' \
+// RUN:  --timeout 90 \
+// RUN:  || true) \
+// RUN:  > $outfile \
+// RUN:  2>&1
+// RUN: FileCheck %s < $outfile
+// if [ -z ${LAKEROAD_PRIVATE_DIR+x} ]; then \
+//   echo "Warning: LAKEROAD_PRIVATE_DIR is not set. Skipping simulation."; \
+//   exit 0; \
+// else \
+//   python3 $LAKEROAD_DIR/bin/simulate_with_verilator.py \
+//    --test_module_name out \
+//    --ground_truth_module_name top \
+//    --max_num_tests=10000 \
+//    --verilog_filepath $outfile \
+//    --verilog_filepath %s \
+//    --pipeline_depth 0 \
+//    --output_signal out:48 \
+//    --input_signal c:47 \
+//    --verilator_include_dir "$LAKEROAD_PRIVATE_DIR/DSP48E2/" \
+//    --verilator_extra_arg='-DXIL_XECLIB' \
+//    --verilator_extra_arg='-Wno-UNOPTFLAT' \
+//    --verilator_extra_arg='-Wno-LATCH' \
+//    --verilator_extra_arg='-Wno-WIDTH' \
+//    --verilator_extra_arg='-Wno-STMTDLY' \
+//    --verilator_extra_arg='-Wno-CASEX' \
+//    --verilator_extra_arg='-Wno-TIMESCALEMOD' \
+//    --verilator_extra_arg='-Wno-PINMISSING'; \
+// fi
+
+// TODO(@gussmith23): For some reason, this doesn't work with c of length 48.
+// Works with 47 though.
+module top(input [47:0] c, output [47:0] out);
+  assign out = 48'(48'(c) >> 17);
+endmodule
+
+// CHECK: Synthesis failed
\ No newline at end of file
diff --git a/integration_tests/lakeroad/xilinx_ultrascale_plus_dsp_internal_shift_explicit_arithmetic_shift.v b/integration_tests/lakeroad/xilinx_ultrascale_plus_dsp_internal_shift_explicit_arithmetic_shift.v
new file mode 100644
index 00000000..4b69fd4c
--- /dev/null
+++ b/integration_tests/lakeroad/xilinx_ultrascale_plus_dsp_internal_shift_explicit_arithmetic_shift.v
@@ -0,0 +1,51 @@
+// RUN: outfile=$(mktemp)
+// RUN: racket $LAKEROAD_DIR/bin/main.rkt \
+// RUN:  --solver bitwuzla \
+// RUN:  --verilog-module-filepath %s \
+// RUN:  --architecture xilinx-ultrascale-plus \
+// RUN:  --template dsp \
+// RUN:  --out-format verilog \
+// RUN:  --top-module-name top \
+// RUN:  --verilog-module-out-signal out:48 \
+// RUN:  --pipeline-depth 0 \
+// RUN:  --module-name out \
+// RUN:  --input-signal 'c:(port c 48):48' \
+// RUN:  --timeout 90 \
+// RUN: > $outfile
+// RUN: FileCheck %s < $outfile
+// RUN: if [ -z ${LAKEROAD_PRIVATE_DIR+x} ]; then \
+// RUN:   echo "Warning: LAKEROAD_PRIVATE_DIR is not set. Skipping simulation."; \
+// RUN:   exit 0; \
+// RUN: else \
+// RUN:   python3 $LAKEROAD_DIR/bin/simulate_with_verilator.py \
+// RUN:    --test_module_name out \
+// RUN:    --ground_truth_module_name top \
+// RUN:    --max_num_tests=10000 \
+// RUN:    --verilog_filepath $outfile \
+// RUN:    --verilog_filepath %s \
+// RUN:    --pipeline_depth 0 \
+// RUN:    --output_signal out:48 \
+// RUN:    --input_signal c:48 \
+// RUN:    --verilator_include_dir "$LAKEROAD_PRIVATE_DIR/DSP48E2/" \
+// RUN:    --verilator_extra_arg='-DXIL_XECLIB' \
+// RUN:    --verilator_extra_arg='-Wno-UNOPTFLAT' \
+// RUN:    --verilator_extra_arg='-Wno-LATCH' \
+// RUN:    --verilator_extra_arg='-Wno-WIDTH' \
+// RUN:    --verilator_extra_arg='-Wno-STMTDLY' \
+// RUN:    --verilator_extra_arg='-Wno-CASEX' \
+// RUN:    --verilator_extra_arg='-Wno-TIMESCALEMOD' \
+// RUN:    --verilator_extra_arg='-Wno-PINMISSING'; \
+// RUN: fi
+
+// TODO(@gussmith23): here, I explicitly do a signed shift, which does
+// synthesize. I assumed >> did a signed shift when the arguments are signed,
+// but perhaps I'm wrong. Why does this matter? Because it means we need to be
+// careful about how we do our rewriting in the egraph. We can't necessarily
+// just rewrite to a >> in the egraph without fully understanding the semantics.
+// So the task here is to understand how we should be writing the shift 
+// in a partial-product multiply-splitting scenario.
+module top(input [47:0] c, output [47:0] out);
+  assign out = {{17{c[47]}}, c[47:17]};
+endmodule
+
+// CHECK: module out(c, out);
\ No newline at end of file
diff --git a/integration_tests/lakeroad/xilinx_ultrascale_plus_mac_with_internal_shift.v b/integration_tests/lakeroad/xilinx_ultrascale_plus_mac_with_internal_shift.v
new file mode 100644
index 00000000..9f309b51
--- /dev/null
+++ b/integration_tests/lakeroad/xilinx_ultrascale_plus_mac_with_internal_shift.v
@@ -0,0 +1,49 @@
+// RUN: outfile=$(mktemp)
+// RUN: racket $LAKEROAD_DIR/bin/main.rkt \
+// RUN:  --solver cvc5 \
+// RUN:  --verilog-module-filepath %s \
+// RUN:  --architecture xilinx-ultrascale-plus \
+// RUN:  --template dsp \
+// RUN:  --out-format verilog \
+// RUN:  --top-module-name top \
+// RUN:  --verilog-module-out-signal out:48 \
+// RUN:  --pipeline-depth 0 \
+// RUN:  --module-name out \
+// RUN:  --input-signal 'a:(port a 16):16' \
+// RUN:  --input-signal 'b:(port b 16):16' \
+// RUN:  --input-signal 'c:(port c 48):48' \
+// RUN:  --timeout 90 \
+// RUN: > $outfile
+// RUN: FileCheck %s < $outfile
+// RUN: if [ -z ${LAKEROAD_PRIVATE_DIR+x} ]; then \
+// RUN:   echo "Warning: LAKEROAD_PRIVATE_DIR is not set. Skipping simulation."; \
+// RUN:   exit 0; \
+// RUN: else \
+// RUN:   python3 $LAKEROAD_DIR/bin/simulate_with_verilator.py \
+// RUN:    --test_module_name out \
+// RUN:    --ground_truth_module_name top \
+// RUN:    --max_num_tests=10000 \
+// RUN:    --verilog_filepath $outfile \
+// RUN:    --verilog_filepath %s \
+// RUN:    --pipeline_depth 0 \
+// RUN:    --output_signal out:48 \
+// RUN:    --input_signal a:30 \
+// RUN:    --input_signal b:18 \
+// RUN:    --input_signal c:48 \
+// RUN:    --verilator_include_dir "$LAKEROAD_PRIVATE_DIR/DSP48E2/" \
+// RUN:    --verilator_extra_arg='-DXIL_XECLIB' \
+// RUN:    --verilator_extra_arg='-Wno-UNOPTFLAT' \
+// RUN:    --verilator_extra_arg='-Wno-LATCH' \
+// RUN:    --verilator_extra_arg='-Wno-WIDTH' \
+// RUN:    --verilator_extra_arg='-Wno-STMTDLY' \
+// RUN:    --verilator_extra_arg='-Wno-CASEX' \
+// RUN:    --verilator_extra_arg='-Wno-TIMESCALEMOD' \
+// RUN:    --verilator_extra_arg='-Wno-PINMISSING'; \
+// RUN: fi
+
+module top(input [15:0] a, input [15:0] b, input [47:0] c, output [47:0] out);
+  logic [31:0] mul_result = a * b;
+  assign out = mul_result + {{17{c[47]}}, c[47:17]};
+endmodule
+
+// CHECK: module out(a, b, c, out);
\ No newline at end of file