diff --git a/include/souper/Infer/InstSynthesis.h b/include/souper/Infer/InstSynthesis.h
index 1db4100e8..e17578a93 100644
--- a/include/souper/Infer/InstSynthesis.h
+++ b/include/souper/Infer/InstSynthesis.h
@@ -132,6 +132,9 @@ class InstSynthesis {
                              const BlockPCs &BPCs,
                              const std::vector<InstMapping> &PCs,
                              Inst *TargetLHS, Inst *&RHS,
+                             const std::vector<Inst *> &Copies,
+                             const std::vector<InstMapping> &PCsCopy,
+                             const BlockPCs &BPCsCopy,
                              InstContext &IC, unsigned Timeout);
 
 private:
diff --git a/lib/Extractor/Solver.cpp b/lib/Extractor/Solver.cpp
index 3e0a7d50c..9db062c1b 100644
--- a/lib/Extractor/Solver.cpp
+++ b/lib/Extractor/Solver.cpp
@@ -206,8 +206,24 @@ class BaseSolver : public Solver {
     }
 
     if (InferInsts && SMTSolver->supportsModels()) {
+      std::vector<Inst *> LHSComps;
+      findCands(LHS, LHSComps, IC, MaxNops);
+
+      std::vector<Inst *> Copies;
+      std::vector<InstMapping> PCsCopy;
+      BlockPCs BPCsCopy;
+      for (auto I : LHSComps) {
+        // separate sub-expressions by copying vars
+        std::map<Inst *, Inst *> InstCache;
+        std::map<Block *, Block *> BlockCache;
+        Copies.push_back(getInstCopy(I, IC, InstCache, BlockCache));
+        separateBlockPCs(BPCs, BPCsCopy, InstCache, BlockCache, IC);
+        separatePCs(PCs, PCsCopy, InstCache, BlockCache, IC);
+      }
+
       InstSynthesis IS;
-      EC = IS.synthesize(SMTSolver.get(), BPCs, PCs, LHS, RHS, IC, Timeout);
+      EC = IS.synthesize(SMTSolver.get(), BPCs, PCs, LHS, RHS,
+                         Copies, PCsCopy, BPCsCopy, IC, Timeout);
       if (EC || RHS)
         return EC;
     }
diff --git a/lib/Infer/InstSynthesis.cpp b/lib/Infer/InstSynthesis.cpp
index a6281ecbb..7c6c0e2d8 100644
--- a/lib/Infer/InstSynthesis.cpp
+++ b/lib/Infer/InstSynthesis.cpp
@@ -59,6 +59,9 @@ std::error_code InstSynthesis::synthesize(SMTLIBSolver *SMTSolver,
                                           const BlockPCs &BPCs,
                                           const std::vector<InstMapping> &PCs,
                                           Inst *TargetLHS, Inst *&RHS,
+                                          const std::vector<Inst *> &Copies,
+                                          const std::vector<InstMapping> &PCsCopy,
+                                          const BlockPCs &BPCsCopy,
                                           InstContext &IC, unsigned Timeout) {
   std::error_code EC;