diff --git a/Parse/SMTLIB2.cpp b/Parse/SMTLIB2.cpp
index 2d8d3d111e..5bbc5c249a 100644
--- a/Parse/SMTLIB2.cpp
+++ b/Parse/SMTLIB2.cpp
@@ -221,6 +221,19 @@ void SMTLIB2::readBenchmark(LExpr* bench)
       continue;
     }
 
+    if (ibRdr.tryAcceptAtom("define-const")) {
+
+      auto name = ibRdr.readAtom();
+      auto oSort = ibRdr.readExpr();
+      auto body = ibRdr.readExpr();
+      LExpr iArgs(LispParser::LIST); // dummy list to avoid passing null below
+      readDefineFun(name,&iArgs,oSort,body,/*recursive=*/false);
+
+      ibRdr.acceptEOL();
+
+      continue;
+    }
+
     bool recursive = false;
     if (ibRdr.tryAcceptAtom("define-fun") || (recursive = ibRdr.tryAcceptAtom("define-fun-rec"))) {
 
diff --git a/checks/parse/define-const.smt2 b/checks/parse/define-const.smt2
new file mode 100644
index 0000000000..3d27da115d
--- /dev/null
+++ b/checks/parse/define-const.smt2
@@ -0,0 +1,4 @@
+(define-const c Int 5)
+(define-fun double ((x Int)) Int (* 2 x))
+(assert (not (= (+ (double c) (double c)) (double (+ c c)))))
+(check-sat)
\ No newline at end of file
diff --git a/checks/sanity b/checks/sanity
index fb8b6f713e..f60e76c5f2 100755
--- a/checks/sanity
+++ b/checks/sanity
@@ -115,6 +115,7 @@ check_szs_status Unsatisfiable -newcnf on -t 1 parse/smtlib2-parametric-datatype
 check_szs_status Unsatisfiable parse/smtlib2-mutual-recursion.smt2
 check_szs_status Unsatisfiable -newcnf on parse/let-bind-variable.smt2
 check_szs_status Unsatisfiable -qa synthesis parse/assert-synth-max5.smt2
+check_szs_status Unsatisfiable parse/define-const.smt2
 
 # Arithmetic
 check_szs_status Theorem -t 1d -s 32 -tgt ground -sas z3 -tha some -nm 6 Problems/ANA/ANA135_1.p