diff --git a/rundse/build.gradle b/rundse/build.gradle
index 49bc159bc6d02c39b3556520f355c6edbd989e84..ed941fa63fb3b40cd263453fbfa77c617034ecf1 100644
--- a/rundse/build.gradle
+++ b/rundse/build.gradle
@@ -24,6 +24,7 @@ dependencies {
     compileOnly name:'batik-dom'
     compileOnly name:'batik-util'
     compile name:'jautomata-core'
+    compile name:'com.microsoft.z3'
 }
 
 jar {
diff --git a/rundse/manifest.txt b/rundse/manifest.txt
index 18e66503cd6d4de0cbbbfb608a66e099d2efef45..7ae7016992ad1704b32de0b058f74780cc53c74a 100755
--- a/rundse/manifest.txt
+++ b/rundse/manifest.txt
@@ -1 +1,2 @@
 Main-Class: RunDSE
+Class-Path: com.microsoft.z3.jar
diff --git a/src/main/java/ui/ActionPerformer.java b/src/main/java/ui/ActionPerformer.java
index 18d5b9846f93578b73756508ff36bfa24be0aa96..28bb9705c00b458e1cc11704bc19044df6d05901 100644
--- a/src/main/java/ui/ActionPerformer.java
+++ b/src/main/java/ui/ActionPerformer.java
@@ -173,6 +173,10 @@ public class ActionPerformer {
             mgui.generateUPPAAL();
         } else if (command.equals(mgui.actions[TGUIAction.ACT_DSE].getActionCommand())) {
             mgui.dse();
+        } else if (command.equals(mgui.actions[TGUIAction.ACT_DSE_Z3].getActionCommand())) {
+            mgui.dseZ3();
+        } else if (command.equals(mgui.actions[TGUIAction.ACT_DSE].getActionCommand())) {
+            mgui.dse();
         } else if (command.equals(mgui.actions[TGUIAction.ACT_AVATAR_MODEL_CHECKER].getActionCommand())) {
             mgui.avatarModelChecker();
         } else if (command.equals(mgui.actions[TGUIAction.ACT_GEN_JAVA].getActionCommand())) {
diff --git a/src/main/java/ui/JToolBarMainTurtle.java b/src/main/java/ui/JToolBarMainTurtle.java
index c926eb9a104cebe3d3c88729ee8dae247eeed35a..69dc3d24ac599c7896ed37580b1ed5e2fe3076c3 100644
--- a/src/main/java/ui/JToolBarMainTurtle.java
+++ b/src/main/java/ui/JToolBarMainTurtle.java
@@ -64,7 +64,7 @@ public  class JToolBarMainTurtle extends JToolBar implements ActionListener
     JButton  avatarSimu, avatarFVUPPAAL, avatarFVProVerif, avatarFVStaticAnalysis, avatarCodeGeneration, avatarMC;
 
     // Other
-    JButton genrtlotos, genlotos, genuppaal, gendesign, dse;
+    JButton genrtlotos, genlotos, genuppaal, gendesign, dse, dseZ3;
     JButton checkcode, simulation, validation;
     JButton oneClickrtlotos, onclicklotos, gensystemc, simusystemc, gentml, genC, genjava, nc,externalSearch, internalSearch;
 
@@ -166,6 +166,11 @@ public  class JToolBarMainTurtle extends JToolBar implements ActionListener
         dse = add(mgui.actions[TGUIAction.ACT_DSE]);
         dse.addMouseListener(mgui.mouseHandler);
 
+        if (MainGUI.experimentalOn) {
+            dseZ3 = add(mgui.actions[TGUIAction.ACT_DSE_Z3]);
+            dseZ3.addMouseListener(mgui.mouseHandler);
+        }
+
         addSeparator();
 
         //if (MainGUI.experimentalOn) {
@@ -318,6 +323,7 @@ public  class JToolBarMainTurtle extends JToolBar implements ActionListener
 
         //TraceManager.addDev("Show avatar options with b = " + b);
         dse.setVisible(!b);
+        dseZ3.setVisible(!b);
 
         avatarSimu.setVisible(b);
         avatarFVUPPAAL.setVisible(b);
@@ -395,6 +401,7 @@ public  class JToolBarMainTurtle extends JToolBar implements ActionListener
         //TraceManager.addDev("Show diplodocus options with b = " + b);
 
         dse.setVisible(b);
+        dseZ3.setVisible(b);
         avatarSimu.setVisible(!b);
         avatarFVUPPAAL.setVisible(!b);
         avatarFVStaticAnalysis.setVisible(!b);
diff --git a/src/main/java/ui/MainGUI.java b/src/main/java/ui/MainGUI.java
index 277aad5242a9579b53a0de7f4b2f28ed5f640ce5..95e6711332a6b0ff14bdeebc9e877bb2270ba9bf 100644
--- a/src/main/java/ui/MainGUI.java
+++ b/src/main/java/ui/MainGUI.java
@@ -4793,6 +4793,15 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
         dtree.toBeUpdated();
     }
 
+    public void dseZ3() {
+        TraceManager.addDev("Design space exploration with Z3");
+        /*JDialogDSE jdse = new JDialogDSE(frame, this, "Design Space Exploration", SpecConfigTTool.SystemCCodeDirectory, SpecConfigTTool.TMLCodeDirectory);
+        //   jdse.setSize(600,800);
+        GraphicLib.centerOnParent(jdse, 700, 800);
+        jdse.setVisible(true);
+        dtree.toBeUpdated();*/
+    }
+
     public void avatarStaticAnalysis() {
         TraceManager.addDev("Avatar static analysis invariants");
         JDialogInvariantAnalysis jgen = new JDialogInvariantAnalysis(frame, this, "Static analysis: invariants computation");
diff --git a/src/main/java/ui/ModeManager.java b/src/main/java/ui/ModeManager.java
index d771aec8268fe34be460b41fd63a79520aadd676..37712ad69d103a0ecdd2a500864568d96d4df278 100644
--- a/src/main/java/ui/ModeManager.java
+++ b/src/main/java/ui/ModeManager.java
@@ -144,6 +144,7 @@ public class ModeManager {
                 actions[TGUIAction.ACT_GEN_RTLOTOS].setEnabled(true);
                 actions[TGUIAction.ACT_GEN_LOTOS].setEnabled(true);
                 actions[TGUIAction.ACT_DSE].setEnabled(true);
+                actions[TGUIAction.ACT_DSE_Z3].setEnabled(true);
                 if (mgui.getCurrentTURTLEPanel() instanceof TMLComponentDesignPanel) {
                     actions[TGUIAction.ACT_GEN_UPPAAL].setEnabled(true);
                 } else {
@@ -228,6 +229,7 @@ public class ModeManager {
                 actions[TGUIAction.ACT_GEN_RTLOTOS].setEnabled(false);
                 actions[TGUIAction.ACT_GEN_LOTOS].setEnabled(false);
                 actions[TGUIAction.ACT_DSE].setEnabled(false);
+                actions[TGUIAction.ACT_DSE_Z3].setEnabled(false);
                 actions[TGUIAction.ACT_GEN_JAVA].setEnabled(false);
                 actions[TGUIAction.ACT_SIMU_JAVA].setEnabled(false);
                 actions[TGUIAction.ACT_GEN_DESIGN].setEnabled(false);
@@ -252,6 +254,7 @@ public class ModeManager {
                 actions[TGUIAction.ACT_GEN_RTLOTOS].setEnabled(false);
                 actions[TGUIAction.ACT_GEN_LOTOS].setEnabled(false);
                 actions[TGUIAction.ACT_DSE].setEnabled(false);
+                actions[TGUIAction.ACT_DSE_Z3].setEnabled(false);
                 actions[TGUIAction.ACT_CHECKCODE].setEnabled(false);
                 actions[TGUIAction.ACT_SIMULATION].setEnabled(false);
                 actions[TGUIAction.ACT_VALIDATION].setEnabled(false);
@@ -272,6 +275,7 @@ public class ModeManager {
                 actions[TGUIAction.ACT_GEN_RTLOTOS].setEnabled(false);
                 actions[TGUIAction.ACT_GEN_LOTOS].setEnabled(false);
                 actions[TGUIAction.ACT_DSE].setEnabled(false);
+                actions[TGUIAction.ACT_DSE_Z3].setEnabled(false);
                 actions[TGUIAction.ACT_GEN_JAVA].setEnabled(false);
                 actions[TGUIAction.ACT_SIMU_JAVA].setEnabled(false);
                 actions[TGUIAction.ACT_GEN_DESIGN].setEnabled(false);
diff --git a/src/main/java/ui/TGUIAction.java b/src/main/java/ui/TGUIAction.java
index 2b4bfd066bbf84e9c886fbb8562a7ecd1e3249a7..6defdce51bbd17189e592a6bfd472366d62dbde9 100644
--- a/src/main/java/ui/TGUIAction.java
+++ b/src/main/java/ui/TGUIAction.java
@@ -649,6 +649,7 @@ public class TGUIAction extends AbstractAction {
     public static final int ACT_AVATAR_EXECUTABLE_GENERATION = 340;
 
     public static final int ACT_DSE = 434;
+    public static final int ACT_DSE_Z3 = 516;
 
     // Ontologies
     public static final int ACT_GENERATE_ONTOLOGIES_CURRENT_DIAGRAM = 367;
@@ -667,7 +668,7 @@ public class TGUIAction extends AbstractAction {
     public static final int MOVE_ENABLED = 463;
     public static final int FIRST_DIAGRAM = 464;
     
-    public static final int NB_ACTION = 516;
+    public static final int NB_ACTION = 517;
 
     private static final TAction [] actions = new TAction[NB_ACTION];
 
@@ -866,7 +867,9 @@ public class TGUIAction extends AbstractAction {
         actions[ACT_VIEW_PM_AUT] = new TAction("viewpmaut-command", "Power Management Analysis (last AUT graph)", IconManager.imgic28, IconManager.imgic29, "Power Management Analysis (last AUT graph)",  "Power Management Analysis on the last generated reachability graph generated in AUT (Aldebaran) format", 0);
         actions[ACT_VIEW_PM_AUTPROJ] = new TAction("viewpmautproj-command", "Power Management Analysis (last minimized AUT graph)", IconManager.imgic28, IconManager.imgic29, "Power Management Analysis (last minimized AUT graph)",  "Power Management Analysis on the last minimized reachability graph  in AUT (Aldebaran) format", 0);
         actions[ACT_VIEW_PM_SAVED_AUT] = new TAction("viewpmsavedautproj-command", "Power Management Analysis (saved AUT graph)", IconManager.imgic28, IconManager.imgic29, "Power Management Analysis (saved AUT graph)",  "Power Management Analysis on a graph saved in AUT (Aldebaran) format", 0);
-        actions[ACT_DSE] = new TAction("auto-dse", "Automated Design Space Exploration", IconManager.imgic89, IconManager.imgic89, "Automated Design Space Exploration", "Find the optimal mapping and security additions automatically",0);
+        actions[ACT_DSE] = new TAction("auto-dse", "Automated Design Space Exploration", IconManager.imgic89, IconManager.imgic89, "Automated Design Space Exploration", "Find the optimal mapping with brute-force simulations",0);
+        actions[ACT_DSE_Z3] = new TAction("auto-dse-z3", "Automated Design Space Exploration with Z3", IconManager.imgic89_z3, IconManager.imgic89_z3, "Automated Design Space Exploration with Z3", "Find the optimal mapping with Z3",0);
+
         // AVATAR
         actions[ACT_AVATAR_SIM] = new TAction("avatar-simu", "Interactive simulation", IconManager.imgic18, IconManager.imgic18, "Interactive simulation",  "Interactive simulation of the AVATAR design under edition", '2');
         actions[ACT_AVATAR_FV_UPPAAL] = new TAction("avatar-formal-verification-uppaal", "Safety formal verification with UPPAAL (Safety)", IconManager.imgic86, IconManager.imgic86, "Formal verification with UPPAAL (Safety)",  "Formal verification with UPPAAL (Safety) of the AVATAR design under edition", '3');
diff --git a/src/main/java/ui/util/IconManager.java b/src/main/java/ui/util/IconManager.java
index d85639588433221e0c71ba60057ee2823edfe669..0a0a2f1a821671528a0f08908514f33f61c9e7bb 100755
--- a/src/main/java/ui/util/IconManager.java
+++ b/src/main/java/ui/util/IconManager.java
@@ -71,7 +71,7 @@ public class IconManager {
     public static ImageIcon imgic50, imgic51, imgic52, imgic53, imgic54, imgic55, imgic56, imgic57, imgic58, imgic59;
     public static ImageIcon imgic60, imgic61, imgic62, imgic63, imgic64, imgic65, imgic66, imgic68;
     public static ImageIcon imgic70, imgic71, imgic72, imgic73, imgic75, imgic76, imgic77, imgic78, imgic79, imgic780;
-    public static ImageIcon imgic80, imgic82, imgic84, imgic86, imgic88, imgic89;
+    public static ImageIcon imgic80, imgic82, imgic84, imgic86, imgic88, imgic89, imgic89_z3;
     public static ImageIcon imgic90, imgic92, imgic94, imgic96, imgic98, imgic99;
 
     public static ImageIcon imgic142;
@@ -295,6 +295,7 @@ public class IconManager {
     private static String icon86 = "avatarfvuppaal.png";
     private static String icon88 = "avatarfvproverif.png";
     private static String icon89 = "dse.png";
+    private static String icon89_z3 = "dse_z3.png";
     private static String icon90 = "genlotos.gif";
     private static String icon92 = "genuppaal.gif";
     private static String icon94 = "avatarcodegeneration.gif";
@@ -837,6 +838,7 @@ public class IconManager {
         imgic86 = getIcon(icon86);
         imgic88 = getIcon(icon88);
         imgic89 = getIcon(icon89);
+        imgic89_z3 = getIcon(icon89_z3);
         imgic90 = getIcon(icon90);
         imgic92 = getIcon(icon92);
         imgic94 = getIcon(icon94);
diff --git a/src/main/resources/ui/util/dse_z3.png b/src/main/resources/ui/util/dse_z3.png
new file mode 100644
index 0000000000000000000000000000000000000000..9a6a70af8532cb69785839876f2f5e114a1e6ea1
Binary files /dev/null and b/src/main/resources/ui/util/dse_z3.png differ
diff --git a/tmltranslator/build.gradle b/tmltranslator/build.gradle
index 4346731a9719460a767df3c62d32662784a8e812..e03e31b7e47fe6f4b00ca9c441ea77a20a66d77a 100644
--- a/tmltranslator/build.gradle
+++ b/tmltranslator/build.gradle
@@ -25,6 +25,7 @@ dependencies {
     compileOnly name:'batik-util'
     compile name: 'commons-math3-3.6.1'
     compile name: 'jautomata-core'
+    compile name: 'com.microsoft.z3'
 }
 
 jar {
diff --git a/tmltranslator/manifest.txt b/tmltranslator/manifest.txt
index 9c6dd6c3cc95d482fbb78a50590ce6ffd97da599..d0d5ac1d610e1fe17c8652d6d91e40dd1043071d 100755
--- a/tmltranslator/manifest.txt
+++ b/tmltranslator/manifest.txt
@@ -1 +1,2 @@
 Main-Class: TMLTranslator
+Class-Path: com.microsoft.z3.jar