diff --git a/src/main/java/myutil/intboolsovler2/IBSExpression.java b/src/main/java/myutil/intboolsovler2/IBSExpression.java
deleted file mode 100644
index ddc293934e23c79b12ceca16d109ec63740a07d3..0000000000000000000000000000000000000000
--- a/src/main/java/myutil/intboolsovler2/IBSExpression.java
+++ /dev/null
@@ -1,64 +0,0 @@
-package myutil.intboolsovler2;
-
-public class IBSExpression <
-        Spec extends IBSParamSpec,
-        Comp extends IBSParamComp,
-        State extends IBSParamState,
-        SpecState extends IBSParamSpecState,
-        CompState extends IBSParamCompState
-        > {
-    public boolean make_iiiPlus(int _left, int _right, int _tgt) { return false; }
-    public boolean make_iiiMinus(int _left, int _right, int _tgt) { return false; }
-    public boolean make_iiiMult(int _left, int _right, int _tgt) { return false; }
-    public boolean make_iiiDiv(int _left, int _right, int _tgt) { return false; }
-    public boolean make_iiiMod(int _left, int _right, int _tgt) { return false; }
-    public boolean make_bbbAnd(int _left, int _right, int _tgt) { return false; }
-    public boolean make_bbbOr(int _left, int _right, int _tgt) { return false; }
-    public boolean make_biiEq(int _left, int _right, int _tgt) { return false; }
-    public boolean make_bbbEq(int _left, int _right, int _tgt) { return false; }
-    public boolean make_biiDif(int _left, int _right, int _tgt) { return false; }
-    public boolean make_bbbDif(int _left, int _right, int _tgt) { return false; }
-    public boolean make_biiLt(int _left, int _right, int _tgt) { return false; }
-    public boolean make_biiGt(int _left, int _right, int _tgt) { return false; }
-    public boolean make_biiLeq(int _left, int _right, int _tgt) { return false; }
-    public boolean make_biiGeq(int _left, int _right, int _tgt) { return false; }
-    public boolean make_iVar(IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute _v, int _tgt) { return false; }
-    public boolean make_bVar(IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute _v, int _tgt) { return false; }
-    public boolean make_iConst(int _i, int _tgt) { return false; }
-    public boolean make_bConst(boolean _b, int _tgt) { return false; }
-    public boolean make_iNeg(int _expr, int _tgt) throws CloneNotSupportedException  { return false; }
-    public boolean make_bNot(int _expr, int _tgt)  throws CloneNotSupportedException { return false; }
-    public boolean make_biExpr(int _expr, int _tgt) { return false; }
-    public IExpr getIExpr(int _expr) { return null; }
-    public BExpr getBExpr(int _expr) { return null; }
-
-    public abstract class Expr implements Cloneable {
-        public Expr clone() throws CloneNotSupportedException {
-            return (Expr) super.clone();
-        }
-        public abstract String toString();
-        public abstract boolean hasStates();
-        public abstract void linkStates();
-        public abstract void linkComps(Spec _spec);
-    }
-    public abstract class IExpr extends Expr {
-        public IExpr clone() throws CloneNotSupportedException {
-            return (IExpr) super.clone();
-        }
-        public abstract int eval();
-        public abstract int eval(SpecState _ss);
-        public abstract int eval(SpecState _ss, State _st);
-        public abstract int eval(CompState _cs);
-        public abstract int eval(Object _qs);
-    }
-    public abstract class BExpr extends Expr {
-        public BExpr clone() throws CloneNotSupportedException {
-            return (BExpr) super.clone();
-        }
-        public abstract boolean eval();
-        public abstract boolean eval(SpecState _ss);
-        public abstract boolean eval(SpecState _ss, State _st);
-        public abstract boolean eval(CompState _cs);
-        public abstract boolean eval(Object _qs);
-    }
-}
diff --git a/src/main/java/myutil/intboolsovler2/IBSExpressionClass.java b/src/main/java/myutil/intboolsovler2/IBSExpressionClass.java
new file mode 100644
index 0000000000000000000000000000000000000000..9d14b8372cfed589fb8874a533705c7d5bd1cf61
--- /dev/null
+++ b/src/main/java/myutil/intboolsovler2/IBSExpressionClass.java
@@ -0,0 +1,67 @@
+package myutil.intboolsovler2;
+
+public class IBSExpressionClass<
+        Spec extends IBSParamSpec,
+        Comp extends IBSParamComp,
+        State extends IBSParamState,
+        SpecState extends IBSParamSpecState,
+        CompState extends IBSParamCompState
+        > {
+    public final int nbRegisters = 32;
+    public void freeInt(int _toFree) {}
+    public void freeBool(int _toFree) {}
+    public IExpr getIExpr(int _expr) { return null; }
+    public BExpr getBExpr(int _expr) { return null; }
+    public int make_iiiPlus(int _left, int _right) { return -1; }
+    public int make_iiiMinus(int _left, int _right) { return -1; }
+    public int make_iiiMult(int _left, int _right) { return -1; }
+    public int make_iiiDiv(int _left, int _right) { return -1; }
+    public int make_iiiMod(int _left, int _right) { return -1; }
+    public int make_bbbAnd(int _left, int _right) { return -1; }
+    public int make_bbbOr(int _left, int _right) { return -1; }
+    public int make_biiEq(int _left, int _right) { return -1; }
+    public int make_bbbEq(int _left, int _right) { return -1; }
+    public int make_biiDif(int _left, int _right) { return -1; }
+    public int make_bbbDif(int _left, int _right) { return -1; }
+    public int make_biiLt(int _left, int _right) { return -1; }
+    public int make_biiGt(int _left, int _right) { return -1; }
+    public int make_biiLeq(int _left, int _right) { return -1; }
+    public int make_biiGeq(int _left, int _right) { return -1; }
+    public int make_iVar(IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute _v) { return -1; }
+    public int make_bVar(IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute _v) { return -1; }
+    public int make_iConst(int _i) { return -1; }
+    public int make_bConst(boolean _b) { return -1; }
+    public int make_iNeg(int _expr) throws CloneNotSupportedException  { return -1; }
+    public int make_bNot(int _expr)  throws CloneNotSupportedException { return -1; }
+    public int make_biExpr(int _expr) { return -1; }
+
+    public abstract class Expr implements Cloneable {
+        public Expr clone() throws CloneNotSupportedException {
+            return (Expr) super.clone();
+        }
+        public abstract String toString();
+        public abstract boolean hasStates();
+        public abstract void linkStates();
+        public abstract void linkComps(Spec _spec);
+    }
+    public abstract class IExpr extends Expr {
+        public IExpr clone() throws CloneNotSupportedException {
+            return (IExpr) super.clone();
+        }
+        public abstract int eval();
+        public abstract int eval(SpecState _ss);
+        public abstract int eval(SpecState _ss, State _st);
+        public abstract int eval(CompState _cs);
+        public abstract int eval(Object _qs);
+    }
+    public abstract class BExpr extends Expr {
+        public BExpr clone() throws CloneNotSupportedException {
+            return (BExpr) super.clone();
+        }
+        public abstract boolean eval();
+        public abstract boolean eval(SpecState _ss);
+        public abstract boolean eval(SpecState _ss, State _st);
+        public abstract boolean eval(CompState _cs);
+        public abstract boolean eval(Object _qs);
+    }
+}
diff --git a/src/main/java/myutil/intboolsovler2/IBSStdExpression.java b/src/main/java/myutil/intboolsovler2/IBSStdExpressionClass.java
similarity index 82%
rename from src/main/java/myutil/intboolsovler2/IBSStdExpression.java
rename to src/main/java/myutil/intboolsovler2/IBSStdExpressionClass.java
index 2874c169af2e72b00d7826b27ed3a641245695e4..7f600d69444c0f25b29aca94c8214da7b9b25d60 100644
--- a/src/main/java/myutil/intboolsovler2/IBSStdExpression.java
+++ b/src/main/java/myutil/intboolsovler2/IBSStdExpressionClass.java
@@ -2,13 +2,13 @@ package myutil.intboolsovler2;
 
 import java.util.ArrayList;
 
-public class IBSStdExpression<
+public class IBSStdExpressionClass<
         Spec extends IBSParamSpec,
         Comp extends IBSParamComp,
         State extends IBSParamState,
         SpecState extends IBSParamSpecState,
         CompState extends IBSParamCompState
-        > extends IBSExpression<Spec,Comp,State,SpecState,CompState>{
+        > extends IBSExpressionClass<Spec,Comp,State,SpecState,CompState> {
     protected final int[] prios =       { 2 , 2 , 1 , 1 , 1 , 1  ,  2 ,  3 ,  3 ,  3 ,  3 , 3 , 3 ,  3 ,  3 };
     protected final String[] opString = {"+","-","*","/","%","&&","||","==","==","!=","!=","<",">","<=",">=","-","!"};
     public final int iiiPlus = 0;
@@ -34,141 +34,238 @@ public class IBSStdExpression<
     public final int bConst = 1003; // no associated symbol
     public final int biExpr = 1004; // no associated symbol
     
-    private ArrayList<IExpr> iExpressions = new ArrayList<IExpr>();
-    private ArrayList<BExpr> bExpressions = new ArrayList<BExpr>();
-
-    public boolean make_iiiPlus(int _left, int _right, int _tgt) { 
+    private ArrayList<IExpr> iExpressions = new ArrayList<IExpr>(nbRegisters);
+    private boolean[] iBusy = new boolean[nbRegisters];
+    private ArrayList<BExpr> bExpressions = new ArrayList<BExpr>(nbRegisters);
+    private boolean[] bBusy = new boolean[nbRegisters];
+    private int findIfree(){
+        int i;
+        for (i = 0; i < nbRegisters; i++) if (!iBusy[i]) break;
+        if (i==nbRegisters) return -1;
+        return i;
+    }
+    private int findBfree(){
+        int i;
+        for (i = 0; i < nbRegisters; i++) if (!bBusy[i]) break;
+        if (i==nbRegisters) return -1;
+        return i;
+    }
+    public void freeInt(int _toFree) {
+        iBusy[_toFree]=false;
+        iExpressions.set(_toFree,null);
+    }
+    public void freeBool(int _toFree) {
+        bBusy[_toFree]=false;
+        bExpressions.set(_toFree,null);
+    }
+    public int make_iiiPlus(int _left, int _right) {
+        int tgt = findIfree();
+        if ( tgt == -1 ) return -2;
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
-        iExpressions.set(_tgt, new IIIPlus(iExpressions.get(_left), iExpressions.get(_right)));
-        return true;
-    }
-    public boolean make_iiiMinus(int _left, int _right, int _tgt) {
+            return -1;
+        iExpressions.set(tgt, new IIIPlus(iExpressions.get(_left), iExpressions.get(_right)));
+        iBusy[tgt]=true;
+        return tgt;
+    }
+    public int make_iiiMinus(int _left, int _right) {
+        int tgt = findIfree();
+        if ( tgt == -1 ) return -2;
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
-        iExpressions.set(_tgt, new IIIMinus(iExpressions.get(_left), iExpressions.get(_right)));
-        return true;
-    }
-    public boolean make_iiiMult(int _left, int _right, int _tgt) {
+            return -1;
+        iExpressions.set(tgt, new IIIMinus(iExpressions.get(_left), iExpressions.get(_right)));
+        iBusy[tgt]=true;
+        return tgt;
+    }
+    public int make_iiiMult(int _left, int _right) {
+        int tgt = findIfree();
+        if ( tgt == -1 ) return -2;
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
-        iExpressions.set(_tgt, new IIIMult(iExpressions.get(_left), iExpressions.get(_right)));
-        return true;
-    }
-    public boolean make_iiiDiv(int _left, int _right, int _tgt) {
+            return -1;
+        iExpressions.set(tgt, new IIIMult(iExpressions.get(_left), iExpressions.get(_right)));
+        iBusy[tgt]=true;
+        return tgt;
+    }
+    public int make_iiiDiv(int _left, int _right) {
+        int tgt = findIfree();
+        if ( tgt == -1 ) return -2;
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
-        iExpressions.set(_tgt, new IIIDiv(iExpressions.get(_left), iExpressions.get(_right)));
-        return true;
-    }
-    public boolean make_iiiMod(int _left, int _right, int _tgt) {
+            return -1;
+        iExpressions.set(tgt, new IIIDiv(iExpressions.get(_left), iExpressions.get(_right)));
+        iBusy[tgt]=true;
+        return tgt;
+    }
+    public int make_iiiMod(int _left, int _right) {
+        int tgt = findIfree();
+        if ( tgt == -1 ) return -2;
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
-        iExpressions.set(_tgt, new IIIMod(iExpressions.get(_left), iExpressions.get(_right)));
-        return true;
-    }
-    public boolean make_bbbAnd(int _left, int _right, int _tgt) {
+            return -1;
+        iExpressions.set(tgt, new IIIMod(iExpressions.get(_left), iExpressions.get(_right)));
+        iBusy[tgt]=true;
+        return tgt;
+    }
+    public int make_bbbAnd(int _left, int _right) {
+        int tgt = findBfree();
+        if ( tgt == -1 ) return -2;
         if (bExpressions.size()<= _left || bExpressions.size() <= _right || bExpressions.get(_left) == null || bExpressions.get(_right) == null)
-            return false;
-        bExpressions.set(_tgt, new BBBAnd(bExpressions.get(_left), bExpressions.get(_right)));
-        return true;
-    }
-    public boolean make_bbbOr(int _left, int _right, int _tgt) {
+            return -1;
+        bExpressions.set(tgt, new BBBAnd(bExpressions.get(_left), bExpressions.get(_right)));
+        bBusy[tgt]=true;
+        return tgt;
+    }
+    public int make_bbbOr(int _left, int _right) {
+        int tgt = findBfree();
+        if ( tgt == -1 ) return -2;
         if (bExpressions.size()<= _left || bExpressions.size() <= _right || bExpressions.get(_left) == null || bExpressions.get(_right) == null)
-            return false;
-        bExpressions.set(_tgt, new BBBOr(bExpressions.get(_left), bExpressions.get(_right)));
-        return true;
-    }
-    public boolean make_biiEq(int _left, int _right, int _tgt) {
+            return -1;
+        bExpressions.set(tgt, new BBBOr(bExpressions.get(_left), bExpressions.get(_right)));
+        bBusy[tgt]=true;
+        return tgt;
+    }
+    public int make_biiEq(int _left, int _right) {
+        int tgt = findBfree();
+        if ( tgt == -1 ) return -2;
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
-        bExpressions.set(_tgt, new BIIEq(iExpressions.get(_left), iExpressions.get(_right)));
-        return true;
-    }
-    public boolean make_bbbEq(int _left, int _right, int _tgt) {
+            return -1;
+        bExpressions.set(tgt, new BIIEq(iExpressions.get(_left), iExpressions.get(_right)));
+        bBusy[tgt]=true;
+        return tgt;
+    }
+    public int make_bbbEq(int _left, int _right) {
+        int tgt = findBfree();
+        if ( tgt == -1 ) return -2;
         if (bExpressions.size()<= _left || bExpressions.size() <= _right || bExpressions.get(_left) == null || bExpressions.get(_right) == null)
-            return false;
-        bExpressions.set(_tgt, new BBBEq(bExpressions.get(_left), bExpressions.get(_right)));
-        return true;
-    }
-    public boolean make_biiDif(int _left, int _right, int _tgt) {
+            return -1;
+        bExpressions.set(tgt, new BBBEq(bExpressions.get(_left), bExpressions.get(_right)));
+        bBusy[tgt]=true;
+        return tgt;
+    }
+    public int make_biiDif(int _left, int _right) {
+        int tgt = findBfree();
+        if ( tgt == -1 ) return -2;
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
-        bExpressions.set(_tgt, new BIIDif(iExpressions.get(_left), iExpressions.get(_right)));
-        return true;
-    }
-    public boolean make_bbbDif(int _left, int _right, int _tgt) {
+            return -1;
+        bExpressions.set(tgt, new BIIDif(iExpressions.get(_left), iExpressions.get(_right)));
+        bBusy[tgt]=true;
+        return tgt;
+    }
+    public int make_bbbDif(int _left, int _right) {
+        int tgt = findBfree();
+        if ( tgt == -1 ) return -2;
         if (bExpressions.size()<= _left || bExpressions.size() <= _right || bExpressions.get(_left) == null || bExpressions.get(_right) == null)
-            return false;
-        bExpressions.set(_tgt, new BBBDif(bExpressions.get(_left), bExpressions.get(_right)));
-        return true;
-    }
-    public boolean make_biiLt(int _left, int _right, int _tgt) {
+            return -1;
+        bExpressions.set(tgt, new BBBDif(bExpressions.get(_left), bExpressions.get(_right)));
+        bBusy[tgt]=true;
+        return tgt;
+    }
+    public int make_biiLt(int _left, int _right) {
+        int tgt = findBfree();
+        if ( tgt == -1 ) return -2;
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
-        bExpressions.set(_tgt, new BIILt(iExpressions.get(_left), iExpressions.get(_right)));
-        return true;
-    }
-    public boolean make_biiGt(int _left, int _right, int _tgt) {
+            return -1;
+        bExpressions.set(tgt, new BIILt(iExpressions.get(_left), iExpressions.get(_right)));
+        bBusy[tgt]=true;
+        return tgt;
+    }
+    public int make_biiGt(int _left, int _right) {
+        int tgt = findBfree();
+        if ( tgt == -1 ) return -2;
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
-        bExpressions.set(_tgt, new BIIGt(iExpressions.get(_left), iExpressions.get(_right)));
-        return true;
-    }
-    public boolean make_biiLeq(int _left, int _right, int _tgt) {
+            return -1;
+        bExpressions.set(tgt, new BIIGt(iExpressions.get(_left), iExpressions.get(_right)));
+        bBusy[tgt]=true;
+        return tgt;
+    }
+    public int make_biiLeq(int _left, int _right) {
+        int tgt = findBfree();
+        if ( tgt == -1 ) return -2;
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
-        bExpressions.set(_tgt, new BIILeq(iExpressions.get(_left), iExpressions.get(_right)));
-        return true;
-    }
-    public boolean make_biiGeq(int _left, int _right, int _tgt) {
+            return -1;
+        bExpressions.set(tgt, new BIILeq(iExpressions.get(_left), iExpressions.get(_right)));
+        bBusy[tgt]=true;
+        return tgt;
+    }
+    public int make_biiGeq(int _left, int _right) {
+        int tgt = findBfree();
+        if ( tgt == -1 ) return -2;
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
-        bExpressions.set(_tgt, new BIIGeq(iExpressions.get(_left), iExpressions.get(_right)));
-        return true;
-    }
-    public boolean make_iVar(IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute _v, int _tgt) {
+            return -1;
+        bExpressions.set(tgt, new BIIGeq(iExpressions.get(_left), iExpressions.get(_right)));
+        bBusy[tgt]=true;
+        return tgt;
+    }
+    public int make_iVar(IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute _v) {
+        int tgt = findIfree();
+        if ( tgt == -1 ) return -2;
         if (_v == null || _v.getType() != IBSAttributeClass.IntAttr)
-            return false;
-        iExpressions.set(_tgt, new IVar(_v));
-        return true;
-    }
-    public boolean make_bVar(IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute _v, int _tgt) {
+            return -1;
+        iExpressions.set(tgt, new IVar(_v));
+        iBusy[tgt]=true;
+        return tgt;
+    }
+    public int make_bVar(IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute _v) {
+        int tgt = findBfree();
+        if ( tgt == -1 ) return -2;
         if (_v == null || _v.getType() != IBSAttributeClass.BoolAttr)
-            return false;
-        bExpressions.set(_tgt, new BVar(_v));
-        return true;
-    }
-    public boolean make_iConst(int _i, int _tgt) {
-        iExpressions.set(_tgt, new IConst(_i));
-        return true;
-    }
-    public boolean make_bConst(boolean _b, int _tgt) {
-        bExpressions.set(_tgt, new BConst(_b));
-        return true;
-    }
-    public boolean make_iNeg(int _expr, int _tgt) throws CloneNotSupportedException {
+            return -1;
+        bExpressions.set(tgt, new BVar(_v));
+        bBusy[tgt]=true;
+        return tgt;
+    }
+    public int make_iConst(int _i) {
+        int tgt = findIfree();
+        if ( tgt == -1 ) return -2;
+        iExpressions.set(tgt, new IConst(_i));
+        iBusy[tgt]=true;
+        return tgt;
+    }
+    public int make_bConst(boolean _b) {
+        int tgt = findBfree();
+        if ( tgt == -1 ) return -2;
+        bExpressions.set(tgt, new BConst(_b));
+        bBusy[tgt]=true;
+        return tgt;
+    }
+    public int make_iNeg(int _expr) throws CloneNotSupportedException {
+        int tgt = findIfree();
+        if ( tgt == -1 ) return -2;
         if (iExpressions.size()<=_expr || iExpressions.get(_expr) == null)
-            return false;
-        iExpressions.set(_tgt, iExpressions.get(_expr).negate());
-        return true;
-    }
-    public boolean make_bNot(int _expr, int _tgt) throws CloneNotSupportedException {
+            return -1;
+        iExpressions.set(tgt, iExpressions.get(_expr).negate());
+        iBusy[tgt]=true;
+        return tgt;
+    }
+    public int make_bNot(int _expr) throws CloneNotSupportedException {
+        int tgt = findBfree();
+        if ( tgt == -1 ) return -2;
         if (bExpressions.size()<=_expr || bExpressions.get(_expr) == null)
-            return false;
-        bExpressions.set(_tgt, bExpressions.get(_expr).negate());
-        return true;
-    }
-    public boolean make_biExpr(int _expr, int _tgt) {
+            return -1;
+        bExpressions.set(tgt, bExpressions.get(_expr).negate());
+        bBusy[tgt]=true;
+        return tgt;
+    }
+    public int make_biExpr(int _expr) {
+        int tgt = findBfree();
+        if ( tgt == -1 ) return -2;
         if (iExpressions.size()<=_expr || iExpressions.get(_expr) == null)
-            return false;
-        bExpressions.set(_tgt, new BIExpr(iExpressions.get(_expr)));
-        return true;
+            return -1;
+        bExpressions.set(tgt, new BIExpr(iExpressions.get(_expr)));
+        bBusy[tgt]=true;
+        return tgt;
+    }
+    public IExpr getIExpr(int _expr) {
+        if (_expr >= nbRegisters || _expr < 0)
+            return null;
+        else
+            return iExpressions.get(_expr);
+    }
+    public BExpr getBExpr(int _expr) {
+        if (_expr >= nbRegisters || _expr < 0)
+            return null;
+        else
+            return bExpressions.get(_expr);
     }
-    public IExpr getIExpr(int _expr) { return null; }
-    public BExpr getBExpr(int _expr) { return null; }
 
-    public abstract class IExpr extends IBSExpression<Spec,Comp,State,SpecState,CompState>.IExpr {
+    public abstract class IExpr extends IBSExpressionClass<Spec,Comp,State,SpecState,CompState>.IExpr {
         protected int type;
          public boolean isNeg;
          public IExpr clone() throws CloneNotSupportedException {
@@ -182,7 +279,7 @@ public class IBSStdExpression<
         public int getType() { return type; }
         public abstract int getPrio();
     }
-    public abstract class BExpr extends IBSExpression<Spec,Comp,State,SpecState,CompState>.BExpr {
+    public abstract class BExpr extends IBSExpressionClass<Spec,Comp,State,SpecState,CompState>.BExpr {
         protected int type;
         public boolean isNot;
         public BExpr clone() throws CloneNotSupportedException {
diff --git a/src/main/java/myutil/intboolsovler2/OriginExpr.java b/src/main/java/myutil/intboolsovler2/OriginExpr.java
index 8bc751e9ca6c65e217cf548dbe7da7f4a21430c9..be48aa5a4e95e0f75bdc0c2b1519c8b46347c2e3 100644
--- a/src/main/java/myutil/intboolsovler2/OriginExpr.java
+++ b/src/main/java/myutil/intboolsovler2/OriginExpr.java
@@ -39,7 +39,6 @@
 package myutil.intboolsovler2;
 
 import java.util.ArrayList;
-import java.util.HashSet;
 
 /**
  * Class OriginExpr.
@@ -55,240 +54,296 @@ public class OriginExpr<
         State extends IBSParamState,
         SpecState extends IBSParamSpecState,
         CompState extends IBSParamCompState>
-        extends IBSExpression<Spec,Comp,State,SpecState,CompState> {
-    private ArrayList<IExpr> iExpressions = new ArrayList<IExpr>();
-    private ArrayList<BExpr> bExpressions = new ArrayList<BExpr>();
+        extends IBSExpressionClass<Spec,Comp,State,SpecState,CompState> {
+    private ArrayList<IExpr> iExpressions = new ArrayList<IExpr>(nbRegisters);
+    private boolean[] iBusy = new boolean[nbRegisters];
+    private ArrayList<BExpr> bExpressions = new ArrayList<BExpr>(nbRegisters);
+    private boolean[] bBusy = new boolean[nbRegisters];
+    private int findIfree(){
+        int i;
+        for (i = 0; i < nbRegisters; i++) if (!iBusy[i]) break;
+        if (i==nbRegisters) return -1;
+        return i;
+    }
+    private int findBfree(){
+        int i;
+        for (i = 0; i < nbRegisters; i++) if (!bBusy[i]) break;
+        if (i==nbRegisters) return -1;
+        return i;
+    }
+    public void freeInt(int _toFree) {
+        iBusy[_toFree]=false;
+        iExpressions.set(_toFree,null);
+    }
+    public void freeBool(int _toFree) {
+         bBusy[_toFree]=false;
+         bExpressions.set(_toFree,null);
+    }
+    public IExpr getIExpr(int _expr) {
+        if (_expr >= nbRegisters || _expr < 0)
+            return null;
+        else
+            return iExpressions.get(_expr);
+    }
+    public BExpr getBExpr(int _expr) {
+        if (_expr >= nbRegisters || _expr < 0)
+            return null;
+        else
+            return bExpressions.get(_expr);
+    }
 
-    public boolean make_iiiPlus(int _left, int _right, int _tgt) {
+    public int make_iiiPlus(int _left, int _right) {
+        int tgt = findIfree();
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
+            return -1;
         IExpr e = new IExpr();
         e.left = iExpressions.get(_left);
         e.right = iExpressions.get(_right);
         e.operator = '+';
         e.isLeaf = false;
-        iExpressions.set(_tgt,e);
-        return true;
+        iExpressions.set(tgt,e);
+        return tgt;
     }
-    public boolean make_iiiMinus(int _left, int _right, int _tgt) {
+    public int make_iiiMinus(int _left, int _right) {
+        int tgt = findIfree();
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
+            return -1;
         IExpr e = new IExpr();
         e.left = iExpressions.get(_left);
         e.right = iExpressions.get(_right);
         e.operator = '-';
         e.isLeaf = false;
-        iExpressions.set(_tgt,e);
-        return true;
+        iExpressions.set(tgt,e);
+        return tgt;
     }
-    public boolean make_iiiMult(int _left, int _right, int _tgt) {
+    public int make_iiiMult(int _left, int _right) {
+        int tgt = findIfree();
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
+            return -1;
         IExpr e = new IExpr();
         e.left = iExpressions.get(_left);
         e.right = iExpressions.get(_right);
         e.operator = '*';
         e.isLeaf = false;
-        iExpressions.set(_tgt,e);
-        return true;
+        iExpressions.set(tgt,e);
+        return tgt;
     }
-    public boolean make_iiiDiv(int _left, int _right, int _tgt) {
+    public int make_iiiDiv(int _left, int _right) {
+        int tgt = findIfree();
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
+            return -1;
         IExpr e = new IExpr();
         e.left = iExpressions.get(_left);
         e.right = iExpressions.get(_right);
         e.operator = '/';
         e.isLeaf = false;
-        iExpressions.set(_tgt,e);
-        return true;
+        iExpressions.set(tgt,e);
+        return tgt;
     }
-    public boolean make_iiiMod(int _left, int _right, int _tgt) {
+    public int make_iiiMod(int _left, int _right) {
+        int tgt = findIfree();
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
+            return -1;
         IExpr e = new IExpr();
         e.left = iExpressions.get(_left);
         e.right = iExpressions.get(_right);
         e.operator = '%';
         e.isLeaf = false;
-        iExpressions.set(_tgt,e);
-        return true;
+        iExpressions.set(tgt,e);
+        return tgt;
     }
-    public boolean make_bbbAnd(int _left, int _right, int _tgt) {
+    public int make_bbbAnd(int _left, int _right) {
+        int tgt = findBfree();
         if (bExpressions.size()<= _left || bExpressions.size() <= _right || bExpressions.get(_left) == null || bExpressions.get(_right) == null)
-            return false;
+            return -1;
         BExpr e = new BExpr();
         e.type = BExpr.bbb;
         e.bleft = bExpressions.get(_left);
         e.bright = bExpressions.get(_right);
         e.operator = '&';
-        bExpressions.set(_tgt,e);
-        return true;
+        bExpressions.set(tgt,e);
+        return tgt;
     }
-    public boolean make_bbbOr(int _left, int _right, int _tgt) {
+    public int make_bbbOr(int _left, int _right) {
+        int tgt = findBfree();
         if (bExpressions.size()<= _left || bExpressions.size() <= _right || bExpressions.get(_left) == null || bExpressions.get(_right) == null)
-            return false;
+            return -1;
         BExpr e = new BExpr();
         e.type = BExpr.bbb;
         e.bleft = bExpressions.get(_left);
         e.bright = bExpressions.get(_right);
         e.operator = '|';
-        bExpressions.set(_tgt,e);
-        return true;
+        bExpressions.set(tgt,e);
+        return tgt;
     }
-    public boolean make_biiEq(int _left, int _right, int _tgt) {
+    public int make_biiEq(int _left, int _right) {
+        int tgt = findBfree();
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
+            return -1;
         BExpr e = new BExpr();
         e.type = BExpr.bii;
         e.ileft = iExpressions.get(_left);
         e.iright = iExpressions.get(_right);
         e.operator = '=';
-        bExpressions.set(_tgt,e);
-        return true;
+        bExpressions.set(tgt,e);
+        return tgt;
     }
-    public boolean make_bbbEq(int _left, int _right, int _tgt) {
+    public int make_bbbEq(int _left, int _right) {
+        int tgt = findBfree();
         if (bExpressions.size()<= _left || bExpressions.size() <= _right || bExpressions.get(_left) == null || bExpressions.get(_right) == null)
-            return false;
+            return -1;
         BExpr e = new BExpr();
         e.type = BExpr.bbb;
         e.bleft = bExpressions.get(_left);
         e.bright = bExpressions.get(_right);
         e.operator = '=';
-        bExpressions.set(_tgt,e);
-        return true;
+        bExpressions.set(tgt,e);
+        return tgt;
     }
-    public boolean make_biiDif(int _left, int _right, int _tgt) {
+    public int make_biiDif(int _left, int _right) {
+        int tgt = findBfree();
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
+            return -1;
         BExpr e = new BExpr();
         e.type = BExpr.bii;
         e.ileft = iExpressions.get(_left);
         e.iright = iExpressions.get(_right);
         e.operator = '$';
-        bExpressions.set(_tgt,e);
-        return true;
+        bExpressions.set(tgt,e);
+        return tgt;
     }
 
-    public boolean make_bbbDif(int _left, int _right, int _tgt) {
+    public int make_bbbDif(int _left, int _right) {
+        int tgt = findBfree();
         if (bExpressions.size()<= _left || bExpressions.size() <= _right || bExpressions.get(_left) == null || bExpressions.get(_right) == null)
-            return false;
+            return -1;
         BExpr e = new BExpr();
         e.type = BExpr.bbb;
         e.bleft = bExpressions.get(_left);
         e.bright = bExpressions.get(_right);
         e.operator = '$';
-        bExpressions.set(_tgt,e);
-        return true;
+        bExpressions.set(tgt,e);
+        return tgt;
     }
 
-    public boolean make_biiLt(int _left, int _right, int _tgt) {
+    public int make_biiLt(int _left, int _right) {
+        int tgt = findBfree();
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
+            return -1;
         BExpr e = new BExpr();
         e.type = BExpr.bii;
         e.ileft = iExpressions.get(_left);
         e.iright = iExpressions.get(_right);
         e.operator = '<';
-        bExpressions.set(_tgt,e);
-        return true;
+        bExpressions.set(tgt,e);
+        return tgt;
     }
 
-    public boolean make_biiGt(int _left, int _right, int _tgt) {
+    public int make_biiGt(int _left, int _right) {
+        int tgt = findBfree();
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
+            return -1;
         BExpr e = new BExpr();
         e.type = BExpr.bii;
         e.ileft = iExpressions.get(_left);
         e.iright = iExpressions.get(_right);
         e.operator = '>';
-        bExpressions.set(_tgt,e);
-        return true;
+        bExpressions.set(tgt,e);
+        return tgt;
     }
 
-    public boolean make_biiLeq(int _left, int _right, int _tgt) {
+    public int make_biiLeq(int _left, int _right) {
+        int tgt = findBfree();
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
+            return -1;
         BExpr e = new BExpr();
         e.type = BExpr.bii;
         e.ileft = iExpressions.get(_left);
         e.iright = iExpressions.get(_right);
         e.operator = ';';
-        bExpressions.set(_tgt,e);
-        return true;
+        bExpressions.set(tgt,e);
+        return tgt;
     }
 
-    public boolean make_biiGeq(int _left, int _right, int _tgt) {
+    public int make_biiGeq(int _left, int _right) {
+        int tgt = findBfree();
         if (iExpressions.size()<= _left || iExpressions.size() <= _right || iExpressions.get(_left) == null || iExpressions.get(_right) == null)
-            return false;
+            return -1;
         BExpr e = new BExpr();
         e.type = BExpr.bii;
         e.ileft = iExpressions.get(_left);
         e.iright = iExpressions.get(_right);
         e.operator = ':';
-        bExpressions.set(_tgt,e);
-        return true;
+        bExpressions.set(tgt,e);
+        return tgt;
     }
-    public boolean make_iVar(IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute _v, int _tgt) {
+    public int make_iVar(IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute _v) {
+        int tgt = findIfree();
         if (_v == null || _v.getType() != IBSAttributeClass.IntAttr)
-            return false;
+            return -1;
         IExpr e = new IExpr();
         e.leaf = _v;
-        iExpressions.set(_tgt, e);
-        return true;
+        iExpressions.set(tgt, e);
+        return tgt;
     }
-    public boolean make_bVar(IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute _v, int _tgt) {
+    public int make_bVar(IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute _v) {
+        int tgt = findBfree();
         if (_v == null || _v.getType() != IBSAttributeClass.BoolAttr)
-            return false;
+            return -1;
         BExpr e = new BExpr();
         e.type = BExpr.bVar;
         e.leaf = _v;
-        bExpressions.set(_tgt, e);
-        return true;
+        bExpressions.set(tgt, e);
+        return tgt;
     }
 
-    public boolean make_iConst(int _i, int _tgt) {
+    public int make_iConst(int _i) {
+        int tgt = findIfree();
         IExpr e = new IExpr();
         e.isImmediateValue = true; //0: No; 1: Int; 2: Boolean;
         e.intValue = _i;
-        iExpressions.set(_tgt, e);
-        return true;
+        iExpressions.set(tgt, e);
+        return tgt;
     }
 
-    public boolean make_bConst(boolean _b, int _tgt) {
+    public int make_bConst(boolean _b) {
+        int tgt = findBfree();
         BExpr e = new BExpr();
         e.type = BExpr.bCst; //0: No; 1: Int; 2: Boolean;
         e.boolValue = _b;
-        bExpressions.set(_tgt, e);
-        return true;
+        bExpressions.set(tgt, e);
+        return tgt;
     }
-    public boolean make_iNeg(int _expr, int _tgt) throws CloneNotSupportedException {
+    public int make_iNeg(int _expr) throws CloneNotSupportedException {
+        int tgt = findIfree();
         if (iExpressions.size()<=_expr || iExpressions.get(_expr) == null)
-            return false;
+            return -1;
         IExpr e = iExpressions.get(_expr).clone();
         e.isNegated = !iExpressions.get(_expr).isNegated;
-        iExpressions.set(_tgt, e);
-        return true;
+        iExpressions.set(tgt, e);
+        return tgt;
     }
-    public boolean make_bNot(int _expr, int _tgt) throws CloneNotSupportedException {
+    public int make_bNot(int _expr) throws CloneNotSupportedException {
+        int tgt = findBfree();
         if (bExpressions.size()<=_expr || bExpressions.get(_expr) == null)
-            return false;
+            return -1;
         BExpr e = bExpressions.get(_expr).clone();
         e.isNot = !e.isNot;
-        bExpressions.set(_tgt, e);
-        return true;
+        bExpressions.set(tgt, e);
+        return tgt;
     }
-    public boolean make_biExpr(int _expr, int _tgt) {
+    public int make_biExpr(int _expr) {
+        int tgt = findBfree();
         if (iExpressions.size()<=_expr || iExpressions.get(_expr) == null)
-            return false;
+            return -1;
         IExpr expr = iExpressions.get(_expr);
         BExpr e = new BExpr();
         e.type = BExpr.bi;
         e.ileft = expr;
-        bExpressions.set(_tgt, e);
-        return true;
+        bExpressions.set(tgt, e);
+        return tgt;
     }
-    public class IExpr extends IBSExpression<Spec,Comp,State,SpecState,CompState>.IExpr {
+    public class IExpr extends IBSExpressionClass<Spec,Comp,State,SpecState,CompState>.IExpr {
         public IExpr left, right;
         public char operator;
         public boolean isLeaf = true;
@@ -443,7 +498,7 @@ public class OriginExpr<
             }
         }
     }
-    public class BExpr extends IBSExpression<Spec,Comp,State,SpecState,CompState>.BExpr {
+    public class BExpr extends IBSExpressionClass<Spec,Comp,State,SpecState,CompState>.BExpr {
         public static final int bCst = 0;
         public static final int bVar = 1;
         public static final int bii = 2;
diff --git a/src/main/java/myutil/intboolsovler2/OriginParser.java b/src/main/java/myutil/intboolsovler2/OriginParser.java
index d46eab18a5b98566240e73cbec9190e7efb812db..072500baf2a67d1793b7bc353fe4641c6e1ea09e 100644
--- a/src/main/java/myutil/intboolsovler2/OriginParser.java
+++ b/src/main/java/myutil/intboolsovler2/OriginParser.java
@@ -38,8 +38,12 @@
 
 package myutil.intboolsovler2;
 
+import myutil.TraceManager;
+
 import java.util.HashSet;
 
+import static java.lang.Integer.max;
+
 /**
  * Class IBSolver implements the generic solver.
  *
@@ -61,143 +65,383 @@ public class OriginParser<
         SpecState extends IBSParamSpecState,
         CompState extends IBSParamCompState
         > {
-    public  IBSAttributeClass<Spec,Comp,State,SpecState,CompState> attC; // Attribute Class
-    private HashSet<String> freeIdents;
-    public OriginParser(IBSAttributeClass<Spec,Comp,State,SpecState,CompState> _c){
+    public  IBSAttributeClass<Spec,Comp,State,SpecState,CompState> attC;
+    public  IBSExpressionClass<Spec,Comp,State,SpecState,CompState> exprC;
+    private HashSet<String> badIdents;
+    private boolean syntaxError = false;
+
+    public OriginParser(IBSAttributeClass<Spec,Comp,State,SpecState,CompState> _c,
+                        IBSExpressionClass<Spec,Comp,State,SpecState,CompState> _e){
         attC = _c;
-        freeIdents   = new HashSet<String>();
+        exprC = _e;
+        badIdents = new HashSet<String>();
     }
     public OriginParser(){
-        freeIdents   = new HashSet<String>();
+        badIdents = new HashSet<String>();
     }
     public void setAttributeClass(IBSAttributeClass<Spec,Comp,State,SpecState,CompState> _c){
         attC = _c;
     }
     public IBSAttributeClass<Spec,Comp,State,SpecState,CompState> getAttributeClass(){ return attC; }
-    public HashSet<String> getFreeIdents() {
-        return freeIdents;
+    public void setExpressionClass(IBSExpressionClass<Spec,Comp,State,SpecState,CompState> _c){
+        exprC = _c;
+    }
+    public IBSExpressionClass<Spec,Comp,State,SpecState,CompState> getExpressionClass(){ return exprC; }
+    public HashSet<String> getBadIdents() {
+        return badIdents;
     }
-    public void clearFreeIdents() {
-        freeIdents   = new HashSet<String>();
+    public void clearBadIdents() {
+        badIdents.clear();
     }
+    public boolean syntaxError() { return syntaxError; }
 
-    public IBSExpression<Spec,Comp,State,SpecState,CompState>.IExpr
-    parseInt(Spec _spec, String _s) {
-        freeIdents.clear();
+    public IBSExpressionClass<Spec,Comp,State,SpecState,CompState>.IExpr parseInt(Spec _spec, String _s) {
+        badIdents.clear();
+        syntaxError = false;
         attC.initBuild(_spec);
-        return parseIntRec(_spec,_s);
+        int index = parseIntRec(_spec,_s);
+        if (index >= 0) {
+            IBSExpressionClass<Spec, Comp, State, SpecState, CompState>.IExpr res = exprC.getIExpr(index);
+            exprC.freeInt(index);
+            return res;
+        }
+        if (index == -2) TraceManager.addDev("IBSParser: Int Expression Memory Full");
+        return null;
     }
-    public IBSExpression<Spec,Comp,State,SpecState,CompState>.BExpr
-    parseBool(Spec _spec, String _s) {
-        freeIdents.clear();
+    public IBSExpressionClass<Spec,Comp,State,SpecState,CompState>.BExpr parseBool(Spec _spec, String _s) {
+        badIdents.clear();
+        syntaxError = false;
         attC.initBuild(_spec);
-        return parseBoolRec(_spec,_s);
+        int index = parseBoolRec(_spec,_s);
+        if (index >= 0) {
+            IBSExpressionClass<Spec, Comp, State, SpecState, CompState>.BExpr res = exprC.getBExpr(index);
+            exprC.freeBool(index);
+            return res;
+        }
+        if (index == -2) TraceManager.addDev("IBSParser: Int Expression Memory Full");
+        return null;
     }
-    public IBSExpression<Spec,Comp,State,SpecState,CompState>.IExpr
-    parseInt(Comp _comp, String _s) {
-        freeIdents.clear();
+    public IBSExpressionClass<Spec,Comp,State,SpecState,CompState>.IExpr parseInt(Comp _comp, String _s) {
+        badIdents.clear();
+        syntaxError = false;
         attC.initBuild(_comp);
-        return parseIntRec(_comp,_s);
+        int index = parseIntRec(_comp,_s);
+        if (index >= 0) {
+            IBSExpressionClass<Spec, Comp, State, SpecState, CompState>.IExpr res = exprC.getIExpr(index);
+            exprC.freeInt(index);
+            return res;
+        }
+        if (index == -2) TraceManager.addDev("IBSParser: Int Expression Memory Full");
+        return null;
     }
-    public IBSExpression<Spec,Comp,State,SpecState,CompState>.BExpr
-    parseBool(Comp _comp, String _s) {
-        freeIdents.clear();
+    public IBSExpressionClass<Spec,Comp,State,SpecState,CompState>.BExpr parseBool(Comp _comp, String _s) {
+        badIdents.clear();
+        syntaxError = false;
         attC.initBuild(_comp);
-        return parseBoolRec(_comp,_s);
+        int index = parseBoolRec(_comp,_s);
+        if (index >= 0) {
+            IBSExpressionClass<Spec, Comp, State, SpecState, CompState>.BExpr res = exprC.getBExpr(index);
+            exprC.freeBool(index);
+            return res;
+        }
+        if (index == -2) TraceManager.addDev("IBSParser: Int Expression Memory Full");
+        return null;
     }
-    public IBSExpression<Spec,Comp,State,SpecState,CompState>.IExpr
-    parseInt(String _s) {
-        freeIdents.clear();
+    public IBSExpressionClass<Spec,Comp,State,SpecState,CompState>.IExpr parseInt(String _s) {
+        badIdents.clear();
+        syntaxError = false;
         attC.initBuild();
-        return parseIntRec(_s);
+        int index = parseIntRec(_s);
+        if (index >= 0) {
+            IBSExpressionClass<Spec, Comp, State, SpecState, CompState>.IExpr res = exprC.getIExpr(index);
+            exprC.freeInt(index);
+            return res;
+        }
+        if (index == -2) TraceManager.addDev("IBSParser: Int Expression Memory Full");
+        return null;
     }
-    public IBSExpression<Spec,Comp,State,SpecState,CompState>.BExpr
-    parseBool(String _s) {
-        freeIdents.clear();
+    public IBSExpressionClass<Spec,Comp,State,SpecState,CompState>.BExpr parseBool(String _s) {
+        badIdents.clear();
+        syntaxError = false;
         attC.initBuild();
-        return parseBoolRec(_s);
+        int index = parseBoolRec(_s);
+        if (index >= 0) {
+            IBSExpressionClass<Spec, Comp, State, SpecState, CompState>.BExpr res = exprC.getBExpr(index);
+            exprC.freeBool(index);
+            return res;
+        }
+        if (index == -2) TraceManager.addDev("IBSParser: Int Expression Memory Full");
+        return null;
+    }
+    public IBSExpressionClass<Spec,Comp,State,SpecState,CompState>.IExpr
+    makeInt(IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute _attr) {
+        int index = exprC.make_iVar(_attr);
+        if (index >= 0) {
+            IBSExpressionClass<Spec, Comp, State, SpecState, CompState>.IExpr res = exprC.getIExpr(index);
+            exprC.freeInt(index);
+            return res;
+        }
+        if (index == -2) TraceManager.addDev("IBSParser: Int Expression Memory Full");
+        return null;
     }
-    public IBSExpression<Spec,Comp,State,SpecState,CompState>.IExpr
-    intExpr(IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute _attr) {
-            if (_attr==null || _attr.getType() != IBSAttributeClass.IntAttr)
-                return null;
-            return make_iVar(_attr);
+    public IBSExpressionClass<Spec,Comp,State,SpecState,CompState>.BExpr
+    makeBool(IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.Attribute _attr) {
+        int index = exprC.make_bVar(_attr);
+        if (index >= 0) {
+            IBSExpressionClass<Spec, Comp, State, SpecState, CompState>.BExpr res = exprC.getBExpr(index);
+            exprC.freeBool(index);
+            return res;
+        }
+        if (index == -2) TraceManager.addDev("IBSParser: Int Expression Memory Full");
+        return null;
     }
+    private class TestedExpr {
+        public boolean test;
+        public String s;
+        TestedExpr(String _s,boolean _b){ s = _s; test = _b; }
+    }
+    public int parseIntRec(Spec _spec, String _s) {
+        if (_s.matches("^.+[<>=:;\\$&\\|].*$")) {
+            syntaxError = true;
+            return -1;
+        }
 
+        TestedExpr returnVal;
+        String expression = removeUselessBrackets(_s);
+        boolean isNegated = false;
 
-        public boolean buildExpressionRec(Spec _spec) {
-            boolean returnVal;
+        returnVal = checkNegated(expression);
+        if(returnVal==null) return -1;
+        expression = returnVal.s;
+        isNegated = (isNegated != returnVal.test);
 
-            removeUselessBrackets();
-            returnVal = checkNot();
-            returnVal &= checkNegated();
-            if (!returnVal) return false;
+        if (!expression.matches("^.+[\\+\\-\\*/].*$")) {
 
-            if (!expression.matches("^.+[\\+\\-<>=:;\\$&\\|\\*/].*$")) {
-                // leaf
-                isLeaf = true;
-                if (!checkNegatedNoBrackets()) return false;
-                checkNegatedNoBrackets();
-                if (expression.equals("true")) {
-                    intValue = 1;
-                    isImmediateValue = IMMEDIATE_BOOL;
-                    return true;
-                } else if (expression.equals("false")) {
-                    intValue = 0;
-                    isImmediateValue = IMMEDIATE_BOOL;
-                    return true;
-                } else if (expression.matches("-?\\d+")) {
-                    intValue = Integer.parseInt(expression);
-                    isImmediateValue = IMMEDIATE_INT;
-                    return true;
-                } else {
-                    IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.TypedAttribute att =
-                            attC.getTypedAttribute(_spec, expression);
+            returnVal = checkNegated(expression);
+            if(returnVal==null) return -1;
+            expression = returnVal.s;
+            isNegated = (isNegated != returnVal.test);
+
+            if (expression.matches("-?\\d+"))
+                return exprC.make_iConst(Integer.parseInt(expression));
+            else {
+                IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.TypedAttribute att =
+                        attC.getTypedAttribute(_spec, expression);
                     switch (att.getType()) {
-                        case IBSAttributeClass.NullAttr: {
-                            return false;
-                        }
-                        case IBSAttributeClass.BoolConst: {
-                            intValue = att.getConstant();
-                            isImmediateValue = IMMEDIATE_BOOL;
-                            return true;
-                        }
-                        case IBSAttributeClass.IntConst: {
-                            intValue = att.getConstant();
-                            isImmediateValue = IMMEDIATE_INT;
-                            return true;
-                        }
-                        default: {
-                            leaf = att.getAttribute();
-                            return true;
-                        }
+                        case IBSAttributeClass.NullAttr:
+                        case IBSAttributeClass.BoolConst: return -1;
+                        case IBSAttributeClass.IntConst:
+                            return exprC.make_iConst(att.getConstant());
+                        default:
+                            return exprC.make_iVar(att.getAttribute());
                     }
-                }
             }
+        }
+        int index = getOperatorIndex(expression);
+        if (index == -1) return -1;
+
+        String leftExpression = expression.substring(0, index).trim();
+        String rightExpression = expression.substring(index + 1, expression.length()).trim();
+
+        int left  = parseIntRec(_spec,leftExpression);
+        int right = parseIntRec(_spec,rightExpression);
+        if (left<0) {
+            if (right < 0) return max(left, right);
+            exprC.freeInt(right);
+            return left;
+        }
+        switch(expression.charAt(index)) {
+            case '+':
+                return exprC.make_iiiPlus(left, right);
+            case '-':
+                return exprC.make_iiiMinus(left, right);
+            case '*':
+                return exprC.make_iiiMult(left, right);
+            case '/':
+                return exprC.make_iiiDiv(left, right);
+            default: // should not happend
+                syntaxError = true;
+                return -1;
+        }
+    }
+    public int parseIntRec(Comp _comp, String _s) {
+        if (_s.matches("^.+[<>=:;\\$&\\|].*$")) {
+            syntaxError = true;
+            return -1;
+        }
 
-            isLeaf = false;
-
-            int index = getOperatorIndex();
-
-            if (index == -1) {
-                return false;
+        TestedExpr returnVal;
+        String expression = removeUselessBrackets(_s);
+        boolean isNegated = false;
+
+        returnVal = checkNegated(expression);
+        if(returnVal==null) return -1;
+        expression = returnVal.s;
+        isNegated = (isNegated != returnVal.test);
+
+        if (!expression.matches("^.+[\\+\\-\\*/].*$")) {
+
+            returnVal = checkNegated(expression);
+            if(returnVal==null) return -1;
+            expression = returnVal.s;
+            isNegated = (isNegated != returnVal.test);
+
+            if (expression.matches("-?\\d+"))
+                return exprC.make_iConst(Integer.parseInt(expression));
+            else {
+                IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.TypedAttribute att =
+                        attC.getTypedAttribute(_comp, expression);
+                switch (att.getType()) {
+                    case IBSAttributeClass.NullAttr:
+                    case IBSAttributeClass.BoolConst: return -1;
+                    case IBSAttributeClass.IntConst:
+                        return exprC.make_iConst(att.getConstant());
+                    default:
+                        return exprC.make_iVar(att.getAttribute());
+                }
             }
+        }
+        int index = getOperatorIndex(expression);
+        if (index == -1) return -1;
+
+        String leftExpression = expression.substring(0, index).trim();
+        String rightExpression = expression.substring(index + 1, expression.length()).trim();
+
+        int left  = parseIntRec(_comp,leftExpression);
+        int right = parseIntRec(_comp,rightExpression);
+        if (left<0) {
+            if (right < 0) return max(left, right);
+            exprC.freeInt(right);
+            return left;
+        }
+        switch(expression.charAt(index)) {
+            case '+':
+                return exprC.make_iiiPlus(left, right);
+            case '-':
+                return exprC.make_iiiMinus(left, right);
+            case '*':
+                return exprC.make_iiiMult(left, right);
+            case '/':
+                return exprC.make_iiiDiv(left, right);
+            default: // should not happend
+                syntaxError = true;
+                return -1;
+        }
+    }
+    public int parseIntRec(String _s) {
+        if (_s.matches("^.+[<>=:;\\$&\\|].*$")) {
+            syntaxError = true;
+            return -1;
+        }
 
-            operator = expression.charAt(index);
+        TestedExpr returnVal;
+        String expression = removeUselessBrackets(_s);
+        boolean isNegated = false;
 
-            //split and recur
-            String leftExpression = expression.substring(0, index).trim();
-            String rightExpression = expression.substring(index + 1, expression.length()).trim();
+        returnVal = checkNegated(expression);
+        if(returnVal==null) return -1;
+        expression = returnVal.s;
+        isNegated = (isNegated != returnVal.test);
 
-            left = new Expr(leftExpression);
-            right = new Expr(rightExpression);
-            returnVal = left.buildExpressionRec(_spec);
-            returnVal &= right.buildExpressionRec(_spec);
+        if (!expression.matches("^.+[\\+\\-\\*/].*$")) {
 
-            return returnVal;
-        }
+            returnVal = checkNegated(expression);
+            if(returnVal==null) return -1;
+            expression = returnVal.s;
+            isNegated = (isNegated != returnVal.test);
 
-        public boolean buildExpressionRec(Comp _comp) {
+            if (expression.matches("-?\\d+"))
+                return exprC.make_iConst(Integer.parseInt(expression));
+            else
+                return -1;
+        }
+        int index = getOperatorIndex(expression);
+        if (index == -1) return -1;
+
+        String leftExpression = expression.substring(0, index).trim();
+        String rightExpression = expression.substring(index + 1, expression.length()).trim();
+
+        int left  = parseIntRec(leftExpression);
+        int right = parseIntRec(rightExpression);
+        if (left<0) {
+            if (right < 0) return max(left, right);
+            exprC.freeInt(right);
+            return left;
+        }
+        switch(expression.charAt(index)) {
+            case '+':
+                return exprC.make_iiiPlus(left, right);
+            case '-':
+                return exprC.make_iiiMinus(left, right);
+            case '*':
+                return exprC.make_iiiMult(left, right);
+            case '/':
+                return exprC.make_iiiDiv(left, right);
+            default: // should not happend
+                syntaxError = true;
+                return -1;
+        }
+    }
+    public int parseBoolRec(Spec _spec, String _s) {
+        TestedExpr returnVal;
+        String expression = removeUselessBrackets(_s);
+        boolean isNegated = false;
+
+        returnVal = checkNegated(expression);
+        if(returnVal==null) return -1;
+        expression = returnVal.s;
+        isNegated = (isNegated != returnVal.test);
+
+        if (!expression.matches("^.+[\\+\\-\\*/].*$")) {
+
+            returnVal = checkNegated(expression);
+            if(returnVal==null) return -1;
+            expression = returnVal.s;
+            isNegated = (isNegated != returnVal.test);
+
+            if (expression.matches("-?\\d+"))
+                return exprC.make_iConst(Integer.parseInt(expression));
+            else {
+                IBSAttributeClass<Spec,Comp,State,SpecState,CompState>.TypedAttribute att =
+                        attC.getTypedAttribute(_spec, expression);
+                switch (att.getType()) {
+                    case IBSAttributeClass.NullAttr:
+                    case IBSAttributeClass.BoolConst: return -1;
+                    case IBSAttributeClass.IntConst:
+                        return exprC.make_iConst(att.getConstant());
+                    default:
+                        return exprC.make_iVar(att.getAttribute());
+                }
+            }
+        }
+        int index = getOperatorIndex(expression);
+        if (index == -1) return -1;
+
+        String leftExpression = expression.substring(0, index).trim();
+        String rightExpression = expression.substring(index + 1, expression.length()).trim();
+
+        int left  = parseIntRec(_spec,leftExpression);
+        int right = parseIntRec(_spec,rightExpression);
+        if (left<0) {
+            if (right < 0) return max(left, right);
+            exprC.freeInt(right);
+            return left;
+        }
+        switch(expression.charAt(index)) {
+            case '+':
+                return exprC.make_iiiPlus(left, right);
+            case '-':
+                return exprC.make_iiiMinus(left, right);
+            case '*':
+                return exprC.make_iiiMult(left, right);
+            case '/':
+                return exprC.make_iiiDiv(left, right);
+            default: // should not happend
+                syntaxError = true;
+                return -1;
+        }
+    }
+    public boolean buildExpressionRec(Comp _comp) {
             boolean returnVal;
 
             removeUselessBrackets();
@@ -335,7 +579,10 @@ public class OriginParser<
             //expression.replaceAll("\\bfalse\\b", "f").trim();
         }
 
-        private boolean checkNot() {
+        private TestedExpr checkNot(String _s) {
+            String expression = _s;
+            boolean isNot = false;
+
             boolean notStart1, notStart2;
 
             notStart1 = expression.startsWith("not(");
@@ -347,63 +594,70 @@ public class OriginParser<
                     int closingIndex = getClosingBracket(4);
 
                     if (closingIndex == -1) {
-                        return false;
+                        syntaxError=true;
+                        return null;
                     }
                     if (closingIndex == expression.length() - 1) {
                         //not(expression)
                         isNot = !isNot;
                         expression = expression.substring(4, expression.length() - 1).trim();
                     } else {
-                        return true;
+                        return new TestedExpr(expression,isNot);
                     }
                 } else if (notStart2) {
                     int closingIndex = getClosingBracket(2);
 
                     if (closingIndex == -1) {
-                        return false;
+                        syntaxError=true;
+                        return null;
                     }
                     if (closingIndex == expression.length() - 1) {
                         //not(expression)
                         isNot = !isNot;
                         expression = expression.substring(2, expression.length() - 1).trim();
                     } else {
-                        return true;
+                        return new TestedExpr(expression,isNot);
                     }
                 }
                 notStart1 = expression.startsWith("not(");
                 notStart2 = expression.startsWith("!(");
             }
-            return true;
+            return new TestedExpr(expression,isNot);
         }
 
-        private boolean checkNegated() {
-            while (expression.startsWith("-(")) {
+    private TestedExpr checkNegated(String _s) {
+        String expression = _s;
+        boolean isNegated = false;
+        while (expression.startsWith("-(")) {
                 //not bracket must be closed in the last char
                 int closingIndex = getClosingBracket(2);
 
                 if (closingIndex == -1) {
-                    return false;
+                    syntaxError = true;
+                    return null;
                 }
                 if (closingIndex == expression.length() - 1) {
                     //-(expression)
                     isNegated = !isNegated;
                     expression = expression.substring(2, expression.length() - 1).trim();
                 } else {
-                    return true;
+                    return new TestedExpr(expression,isNegated);
                 }
             }
-            return true;
+            return new TestedExpr(expression,isNegated);
         }
 
-        private boolean checkNegatedNoBrackets() {
-            if (expression.startsWith("-")) {
-                isNegated = true;
-                expression = expression.substring(1, expression.length()).trim();
-            }
-            return true;
+    private TestedExpr checkNegatedNoBrackets(String _s) {
+        String expression = _s;
+        boolean isNegated = false;
+        if (expression.startsWith("-")) {
+            isNegated = true;
+            expression = expression.substring(1, expression.length()).trim();
         }
+        return new TestedExpr(expression,isNegated);
+    }
 
-        private int getOperatorIndex() {
+        private int getOperatorIndex(String expression) {
             int index;
             // find the last executed operator
             int i, level, priority;
@@ -799,7 +1053,8 @@ public class OriginParser<
             return returnVal;
         }
 
-        private void removeUselessBrackets() {
+        private String removeUselessBrackets(String _s) {
+            String expression = _s;
             //TraceManager.addDev("Removing first / final brackets");
             while (expression.startsWith("(") && expression.endsWith(")")) {
                 if (getClosingBracket(1) == expression.length() - 1) {
@@ -808,7 +1063,6 @@ public class OriginParser<
                     break;
                 }
             }
-
             //TraceManager.addDev("Removing dual brackets");
             // Removing duplicate brackets
             // typically ((x)) -> (x)
@@ -831,6 +1085,7 @@ public class OriginParser<
                     }
                 }
             }
+            return expression;
         }
 
         private int getClosingBracket(int startChar) {